Mario Carneiro

* [x] depends on #1478 * [ ] depends on #1483 This attribute allows you to specify another declaration to copy the docstring for the given declaration from. Example: ```lean...

Adds support for attributes on `macro`, `elab`, `macro_rules`, `elab_rules`. For `macro` and `elab` the attributes only apply to the `syntax` definition, not the `macro_rules` / `elab_rules` auxiliary definition along with...

* [ ] depends on #1480

Syyntax match does not put info on variables under repetitions

1

```lean syntax "repro" (ident)? ident : command example : Lean.Syntax → Option Lean.Syntax | `(repro $[$x:ident]? a) => x --^ textDocument/hover | `(repro $[$x:ident]? b) => x --^ textDocument/hover --^...

This is an implementation of labeled break and continue in do notation. ```lean example : IO Unit := do for (label := xLoop) x in [1:10] do for (label :=...

Better import errors

4

This is not something I expect to get fixed overnight, but this is an issue to track improvements in import errors. Currently, any errors in file `A` will cause file...

Broken hover in mutual def

2

Currently if you click on `visit` on these lines: https://github.com/leanprover/lean4/blob/9e69259f83432371fdcf3af7ba6f504462e7bff1/src/Lean/MetavarContext.lean#L986-L990 go to definition will take you do this entirely unrelated definition: https://github.com/leanprover/lean4/blob/9e69259f83432371fdcf3af7ba6f504462e7bff1/src/Init/Meta.lean#L229-L230 I suspect it has something to do with...

Do notation inhibits tail call optimization

9

The use of `return` inside `do` notation causes this tail-recursive loop to be compiled into two mutually recursive functions, which breaks TCO. The version using `if-else` instead (`bar` below) optimizes...

`get_unchecked` isn't unchecked

9

This can be seen in the assembly generated by the `get_unchecked` function. Although there is no bounds checking on the array, it still checks whether the entry is occupied and...

Add `truncate_*` operations on `BigInt` and `BigUint`

3

Implements https://github.com/rust-num/num/issues/404