max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add macro_syntax syntax highlight

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-17 13:32:52 -08:00
parent 1b6319788e
commit 5fffecfb53
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lean4-mode/lean4-syntax.el
View file

@ -14,7 +14,7 @@
"open" "export" "axiom" "inductive" "coinductive" "with" "without"
"structure" "universe" "universes" "hide"
"precedence" "reserve"
"match" "nomatch" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
"match_syntax" "match" "nomatch" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
"end" "this" "using" "using_well_founded" "namespace" "section"
"attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
"attributes" "raw" "replacing"