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

feat: add alias bracketedBinder

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-27 19:01:26 -08:00
parent 4ce69bfcab
commit 3d3bed56fd
1 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Parser/Term.lean
View file

@ -219,13 +219,14 @@ end Term
@[builtinTermParser] def Level.quot : Parser := parser! "`(level|" >> toggleInsideQuot levelParser >> ")"
builtin_initialize
registerParserAlias! "letDecl" Term.letDecl
registerParserAlias! "haveDecl" Term.haveDecl
registerParserAlias! "sufficesDecl" Term.sufficesDecl
registerParserAlias! "letRecDecls" Term.letRecDecls
registerParserAlias! "hole" Term.hole
registerParserAlias! "syntheticHole" Term.syntheticHole
registerParserAlias! "matchDiscr" Term.matchDiscr
registerParserAlias! "letDecl" Term.letDecl
registerParserAlias! "haveDecl" Term.haveDecl
registerParserAlias! "sufficesDecl" Term.sufficesDecl
registerParserAlias! "letRecDecls" Term.letRecDecls
registerParserAlias! "hole" Term.hole
registerParserAlias! "syntheticHole" Term.syntheticHole
registerParserAlias! "matchDiscr" Term.matchDiscr
registerParserAlias! "bracketedBinder" Term.bracketedBinder
end Parser
end Lean