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

feat(library/init/lean/parser/term): add ifTerm

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-02 16:29:06 -07:00
parent 56007d7c97
commit 44730314ff
2 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/parser/term.lean
View file

@ -30,6 +30,10 @@ namespace Term
@[builtinTermParser] def cdot := parser! symbol "·" maxPrec
@[inline] def parenSpecial : Parser := optional (", " >> sepBy termParser ", " <|> " : " >> termParser)
@[builtinTermParser] def paren := parser! symbol "(" maxPrec >> optional (termParser >> parenSpecial) >> ")"
@[inline] def optIdent : Parser := optional (try (ident >> " : "))
@[builtinTermParser] def ifTerm := parser! "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
-- @[builtinTermParser] def haveTerm := parser! "have " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
@[builtinTermParser] def app := tparser! pushLeading >> termParser maxPrec

1
tests/playground/termparsertest1.lean
View file

@ -23,4 +23,5 @@ testParser "()";
testParser "(f x)";
testParser "(f x : Type)";
testParser "h (f x) (g y)";
testParser "if x then f x else g x";
pure ()