diff --git a/tests/playground/termparsertest1.lean b/tests/playground/termparsertest1.lean index e35e83b348..ba902e52a5 100644 --- a/tests/playground/termparsertest1.lean +++ b/tests/playground/termparsertest1.lean @@ -9,30 +9,42 @@ termPTables ← builtinTermParsingTable.get; stx ← IO.ofExcept $ runParser env termPTables input "" "expr"; IO.println stx +def test (is : List String) : IO Unit := +is.mfor $ fun input => do + IO.println input; + testParser input + def main (xs : List String) : IO Unit := do -testParser "Prod.mk"; -testParser "x.{u, v+1}"; -testParser "x.{u}"; -testParser "x"; -testParser "x.{max u v}"; -testParser "x.{max u v, 0}"; -testParser "f 0 1"; -testParser "f.{u+1} \"foo\" x"; -testParser "(f x, 0, 1)"; -testParser "()"; -testParser "(f x)"; -testParser "(f x : Type)"; -testParser "h (f x) (g y)"; -testParser "if x then f x else g x"; -testParser "if h : x then f x h else g x h"; -testParser "have p x y from f x; g this"; -testParser "suffices h : p x y from f x; g this"; -testParser "show p x y from f x"; -testParser "fun x y => f y x"; -testParser "fun (x y : Nat) => f y x"; -testParser "fun (x, y) => f y x"; -testParser "fun z (x, y) => f y x"; -testParser "fun ⟨x, y⟩ ⟨z, w⟩ => f y x w z"; -testParser "fun (Prod.mk x y) => f y x"; -pure () +test [ +"Prod.mk", +"x.{u, v+1}", +"x.{u}", +"x", +"x.{max u v}", +"x.{max u v, 0}", +"f 0 1", +"f.{u+1} \"foo\" x", +"(f x, 0, 1)", +"()", +"(f x)", +"(f x : Type)", +"h (f x) (g y)", +"if x then f x else g x", +"if h : x then f x h else g x h", +"have p x y from f x; g this", +"suffices h : p x y from f x; g this", +"show p x y from f x", +"fun x y => f y x", +"fun (x y : Nat) => f y x", +"fun (x, y) => f y x", +"fun z (x, y) => f y x", +"fun ⟨x, y⟩ ⟨z, w⟩ => f y x w z", +"fun (Prod.mk x y) => f y x", +"{ x := 10, y := 20 }", +"{ x := 10, y := 20, }", +"{ x // p x 10 }", +"{ x : Nat // p x 10 }", +"{ .. }", +"{ Prod . fst := 10, .. }" +]