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

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

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-10 15:12:16 -07:00
parent f95ed02999
commit 140cc45491
2 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -78,7 +78,8 @@ def bracktedBinder (requireType := false) := explicitBinder requireType <|> impl
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
def equations : Parser := withPosition $ fun pos => many1 (checkColGe pos.column "'match' cases must be indented" >> equation)
@[builtinTermParser] def «match» := parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> equations
@[builtinTermParser] def «nomatch» := parser! "nomatch " >> termParser
def namedArgument := tparser! try ("(" >> ident >> " := ") >> termParser >> ")"

9
tests/playground/termparsertest1.lean
View file

@ -78,7 +78,14 @@ test [
"
match x with
| some x => true
| none => false"
| none => false",
"
match x with
| some y => match y with
| some (a, b) => a + b
| none => 1
| none => 0
"
];
testFailures [
"f {x : a} -> b",