From 44730314ffef2b5e29317db9e7e411d73e98dc64 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Jul 2019 16:29:06 -0700 Subject: [PATCH] feat(library/init/lean/parser/term): add `ifTerm` --- library/init/lean/parser/term.lean | 4 ++++ tests/playground/termparsertest1.lean | 1 + 2 files changed, 5 insertions(+) diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 084e1f0620..1a815e75ca 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -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 diff --git a/tests/playground/termparsertest1.lean b/tests/playground/termparsertest1.lean index 447e40d037..eb72b435fe 100644 --- a/tests/playground/termparsertest1.lean +++ b/tests/playground/termparsertest1.lean @@ -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 ()