lean.vim

lean.vim copied to clipboard

Lean block comment not correct

1

First of all, thank you for the plugin. I noticed that block comments weren't being highlighted right. The code following the block comment is greyed out. ```lean import .love01_definitions_and_statements_demo /-...

jasoneveleth

Don't highlight fields of things as leanKeyword

1

Right now e.g. `ne.def` will highlight `def` as a `leanKeyword`.

Julian

Add abbreviations

10

This allows vim to replace \pi with Π and similar. Firstly, to allow abbreviations with \\, we need to add \\ to iskeyword, so I modified the syntax file to...

WPettersson