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

feat(library/init/lean/parser/term): explicit universe notation in the new parser

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-02 09:00:58 -07:00
parent 300414e6e4
commit d4a5306d82
2 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -21,7 +21,7 @@ def termParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
namespace Term
@[builtinTermParser] def ident := parser! ident >> optional (".{" >> many1 levelParser >> "}")
@[builtinTermParser] def ident := parser! ident >> optional (".{" >> sepBy1 levelParser ", " >> "}")
@[builtinTermParser] def num : Parser := numLit
@[builtinTermParser] def str : Parser := strLit
@[builtinTermParser] def type := parser! symbol "Type" maxPrec

5
tests/playground/termparsertest1.lean
View file

@ -11,10 +11,11 @@ IO.println stx
def main (xs : List String) : IO Unit :=
do
testParser "x.{u v+1}";
testParser "x.{u, v+1}";
testParser "x.{u}";
testParser "x";
testParser "x.{max u v}";
testParser "x.{(max u v) 0}";
testParser "x.{max u v, 0}";
testParser "f 0 1";
testParser "f.{u+1} \"foo\" x";
testParser "(f x, 0, 1)";