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

feat(library/init/lean/parser/term): match-expression

Browse source 
TODO: add whitespace sensitivity
This commit is contained in:
Leonardo de Moura 2019-07-08 14:14:49 -07:00
parent 5cfa13d08b
commit f37cd3cd11
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -77,6 +77,9 @@ def bracktedBinder (requireType := false) := explicitBinder requireType <|> impl
@[builtinTermParser] def depArrow := parser! bracktedBinder true >> unicodeSymbolCheckPrec " → " " -> " 25 >> termParser
def simpleBinder := parser! many1 binderIdent
@[builtinTermParser] def «forall» := parser! unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracktedBinder) >> ", " >> termParser
def equation := parser! " | " >> sepBy1 termParser ", " >> " => " >> termParser
@[builtinTermParser] def «match» := parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> many1 equation
@[builtinTermParser] def «nomatch» := parser! "nomatch " >> termParser
def namedArgument := tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
@[builtinTermParser] def app := tparser! pushLeading >> (namedArgument <|> termParser appPrec)

6
tests/playground/termparsertest1.lean
View file

@ -74,7 +74,11 @@ test [
"f (x : a) -> b",
"f ((x : a) -> b)",
"(f : (n : Nat) → Vector Nat n) -> Nat",
"∀ x y (z : Nat), x > y -> x > y - z"
"∀ x y (z : Nat), x > y -> x > y - z",
"
match x with
| some x => true
| none => false"
];
testFailures [
"f {x : a} -> b",