lean4

lean4 copied to clipboard

Go-to-definition for types in hover

4

@Kha suggested exploring how *go to definition* could look like for a type shown in a hover. It seems the front end part of this feature would work quite well,...

larsk21

Signature pretty printer

11

In hover text etc., we should not naively print the signature as a term to the right of the colon `:` but move parameters to the left of it, ensuring...

Kha

Server crashes when evaluating missing `extern` definitions

5

### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues). *...

tydeu

Code lense on slow declarations

3

Just testing the waters here: would a code lense showing the processing time for declarations that took more time than `profiler.threshold` be more valuable to mathlib maintainers and authors than...

Kha

Linters

2

We need many different linters. - Style violations. - Common mistakes. - Bad idioms. - Potential performance problems. The different linters can be developed independently of each other, and they...

leodemoura

Syntax autocompletion

1

### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues). *...

lovettchris

Andrew Kent pointed out we were using the `!` for both macros and functions that may panic at runtime. We decided to use it only for functions that panic, and...

leodemoura

String interpolation by default

5

The notation `"..."` would now behave like `s!"..."`, and we would have a notation for raw strings.

leodemoura

### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues). *...

lovettchris

We should add back the Lean 3 behavior of writing the Lean binary's commit hash into each .olean file and checking against it on load, optionally omitting the check during...

Kha