tree-sitter-lean

tree-sitter-lean copied to clipboard

`_dollar` seems to cause the grammar to explode

4

__DISCLAIMER__: I am not a lean expert, I just started to learn it. I was debugging a little the reason why the grammar was extremely long to generate, despite not...

vigoux

```lean def d : OptionM Nat := do let a := (← some 1) let b ← none let c := (← none) + 2 -- this let is not...

gebner

Function application should take precedence over continuing an `open`

5

```lean import Something open Something something " 123 " -- 123 is colored as a number, but should be a string ```

gebner

* [ ] [advent-of-lean-4](https://github.com/rwbarton/advent-of-lean-4) * [ ] [the lean4 topic](https://github.com/topics/lean4) * [ ] [Lean4 itself](https://github.com/leanprover/lean4) * [ ] [mm-lean4](https://github.com/digama0/mm-lean4) * [ ] [mathlib4](https://github.com/leanprover-community/mathlib4) * [ ] mathport

Julian