From 86e1af2066a6109ce50c3413b4604bdd631329dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 19 Jun 2019 14:17:55 -0700
Subject: [PATCH] test(tests/playground/parser1): minor

---
 tests/playground/parser1.lean | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/tests/playground/parser1.lean b/tests/playground/parser1.lean
index f89882111d..c447ef80a5 100644
--- a/tests/playground/parser1.lean
+++ b/tests/playground/parser1.lean
@@ -10,6 +10,10 @@ def mkPairsKind : IO SyntaxNodeKind := nextKind `pairs
 @[init mkPairsKind]
 constant pairsKind : SyntaxNodeKind := default _
 
+def mkFunKind : IO SyntaxNodeKind := nextKind `fun
+@[init mkFunKind]
+constant funKind : SyntaxNodeKind := default _
+
 local infixl `>>`:50 := Lean.Parser.andthen
 
 def pairParser : Parser :=
@@ -20,10 +24,16 @@ attribute [builtinTestParser] pairParser
 
 def pairsParser : Parser :=
 node pairsKind $
-  "{" >> many testParser >> "}"
+  "{" >> many1 testParser >> "}"
 
 attribute [builtinTestParser] pairsParser
 
+def functionParser : Parser :=
+node funKind $
+  "fun" >> ident >> "," >> testParser
+
+attribute [builtinTestParser] functionParser
+
 def testParser (input : String) : IO Unit :=
 do
 env ← mkEmptyEnvironment,
@@ -34,4 +44,4 @@ IO.println stx
 def main (xs : List String) : IO Unit :=
 do
 testParser "(10, hello)",
-testParser "{ (10, hello) /- comment -/ (20, world) { } { (30, foo) } }"
+testParser "{ (10, hello) /- comment -/ (20, world) { fun x, (10, hello) } { (30, foo) } }"