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

feat: add helper syntax

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-10 13:31:45 -07:00
parent 61bd10997a
commit d77dc5efb8
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -244,6 +244,13 @@ stx.isAntiquot || stx.isIdent
@[builtinTermParser] def byTactic := parser!:maxPrec "by " >> Tactic.nonEmptySeq
@[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|" >> toggleInsideQuot funBinder >> ")"
@[builtinTermParser] def panic := parser!:leadPrec "panic! " >> termParser
@[builtinTermParser] def unreachable := parser!:leadPrec "unreachable! " >> termParser
@[builtinTermParser] def dbgTrace := parser!:leadPrec "dbgTrace! " >> termParser >> "; " >> termParser
@[builtinTermParser] def assert := parser!:leadPrec "assert! " >> termParser >> "; " >> termParser
@[builtinTermParser] def «return» := parser!:leadPrec "return " >> termParser
end Term
-- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.quot`