From d77dc5efb8a8d6b26b60ee78767f45c1fadeb906 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Sep 2020 13:31:45 -0700 Subject: [PATCH] feat: add helper syntax --- src/Lean/Parser/Term.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 433a4be18c..e7e1ab8f5c 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -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`