lean4

lean4 copied to clipboard

Antiquotation types silently ignore tokens

4

```lean import Lean open Lean @[defaultInstance] instance : MonadQuotation Elab.TermElabM := inferInstance syntax "👉" (ident "_") : term #eval `(👉 $_) ``` The last underscore has type ``TSyntax `ident``, which...

gebner

`leanc` does not use internal flags when `LEAN_CC` is set even if it is set to the bundled compiler

14

### 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

Unexpected and unnecessary grouping when referring to parsers directly

3

### 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). *...

gebner

Module system enabling separate compilation

5

Currently `import` truly imports everything from a module, including `private` declarations and transitively imported declarations. Thus if we make any change at all that is reflected in the .olean output...

Kha

Goto references does not work for stray files

8

`Goto references` on "foo" doesn't jump to the line of code in bar that is referencing foo. ```lean def foo : Nat := 10 def bar : Nat := foo...

lovettchris

Rules for well-formed parsers

9

With `Parser` and `ParserDescr`/`syntax`, we have two levels of abstraction for defining parsers. In both cases, however, it is possible to define parsers that break as-of-yet unwritten rules, confusing meta...

Kha

Update assignment syntax

11

Compared to languages that allow mutable references for `this/self/...`, updating a mutable variable with the result of one of its "methods" is still a bit verbose in Lean: ```lean references...

Kha

Lean server does not accept `exit` notification before `initialize`

4

### 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

For recursive functions, especially ones that are not trivially structurally recursive, we want to automatically generate induction rules that reflect the function's recursion structure so that proofs over the function...

Kha

RFC: Contextual suggestions

24

# RFC: contextual suggestions  People who are probably interested: @KaseQuark @Kha @javra @Vtec234 @leodemoura @gebner ## Links - [prototype Lean code](https://github.com/Vtec234/npm-widget/blob/5cb1e41aa2a2f597c7821c7b7873316da822ff49/UserWidget/ContextualSuggestion.lean) - [prototype vscode-lean4 code](https://github.com/Vtec234/vscode-lean4/blob/6ab8a5b60c3faca3ed2e1a3674b822ce98e0d08a/lean4-infoview/src/infoview/contextualSuggestions.tsx) ## Goal The purpose...

EdAyers