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

chore: add parser alias matchDiscr

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-17 12:26:29 -08:00
parent f17193e162
commit 4a9c69c7f5
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -218,6 +218,7 @@ builtin_initialize
registerParserAlias! "letRecDecls" Term.letRecDecls
registerParserAlias! "hole" Term.hole
registerParserAlias! "syntheticHole" Term.syntheticHole
registerParserAlias! "matchDiscr" Term.matchDiscr
end Parser
end Lean