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

feat: add nativeDecide! and decide! macros

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-18 15:00:22 -07:00
parent bfe7d1ffe8
commit 77f20d9737
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Lean/Parser/Term.lean
View file

@ -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