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

feat: add named holes notation

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-18 15:13:13 -08:00
parent 42fc213573
commit f852606d13
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/Init/Lean/Parser/Term.lean
View file

@ -41,6 +41,7 @@ def namedPattern := checkNoWsBefore "no space before '@'" >> parser! "@" >> term
@[builtinTermParser] def sort := parser! symbol "Sort" appPrec
@[builtinTermParser] def prop := parser! symbol "Prop" appPrec
@[builtinTermParser] def hole := parser! symbol "_" appPrec
@[builtinTermParser] def namedHole := parser! symbol "?" appPrec >> ident
@[builtinTermParser] def «sorry» := parser! symbol "sorry" appPrec
@[builtinTermParser] def cdot := parser! symbol "·" appPrec
@[builtinTermParser] def emptyC := parser! symbol "∅" appPrec