From 77f20d97370dbc89da06dbd956b202f2dca767dd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Mar 2020 15:00:22 -0700 Subject: [PATCH] feat: add `nativeDecide!` and `decide!` macros --- src/Init/Lean/Parser/Term.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 5ee20c18eb..eafd87cf99 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -137,7 +137,9 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}" @[builtinTermParser] def liftMethod := parser! leftArrow >> termParser @[builtinTermParser] def «do» := parser! symbol "do " leadPrec >> (bracketedDoSeq <|> doSeq) -@[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser appPrec +@[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser appPrec +@[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser appPrec +@[builtinTermParser] def decide := parser! "decide! " >> termParser appPrec @[builtinTermParser] def not := parser! symbol "¬" appPrec >> termParser 40 @[builtinTermParser] def bnot := parser! symbol "!" appPrec >> termParser 40