From c8a045d69fac152fd5e3a577f718615cecb9c53d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 13 Apr 2019 17:07:27 -0700
Subject: [PATCH] test(tests/playground/parser/parser): add `HasAndthen` and
 `HasOrelse` instances

---
 tests/playground/parser/parser.lean | 6 ++++++
 tests/playground/parser/test1.lean  | 4 +---
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/tests/playground/parser/parser.lean b/tests/playground/parser/parser.lean
index 2f4a19b429..0ffc373b60 100644
--- a/tests/playground/parser/parser.lean
+++ b/tests/playground/parser/parser.lean
@@ -677,12 +677,18 @@ end RecParserFn
 @[inline] def andthen {ρ : Type} [ParserFnLift ρ] : AbsParser ρ → AbsParser ρ → AbsParser ρ :=
 mapParser₂ andthenInfo andthenFn
 
+instance absParserAndthen {ρ : Type} [ParserFnLift ρ] : HasAndthen (AbsParser ρ) :=
+⟨andthen⟩
+
 @[inline] def node {ρ : Type} [ParserFnLift ρ] (k : SyntaxNodeKind) : AbsParser ρ → AbsParser ρ :=
 mapParser nodeInfo (nodeFn k)
 
 @[inline] def orelse {ρ : Type} [ParserFnLift ρ] : AbsParser ρ → AbsParser ρ → AbsParser ρ :=
 mapParser₂ orelseInfo orelseFn
 
+instance absParserHasOrelse {ρ : Type} [ParserFnLift ρ] : HasOrelse (AbsParser ρ) :=
+⟨orelse⟩
+
 @[inline] def try {ρ : Type} [ParserFnLift ρ] : AbsParser ρ → AbsParser ρ :=
 mapParser noFirstTokenInfo tryFn
 
diff --git a/tests/playground/parser/test1.lean b/tests/playground/parser/test1.lean
index e8448cdbb6..34327e632c 100644
--- a/tests/playground/parser/test1.lean
+++ b/tests/playground/parser/test1.lean
@@ -1,7 +1,5 @@
 import parser
 open Parser
-local infix ` ; `:10 := Parser.andthen
-local infix ` || `:5 := Parser.orelse
 
 def mkNumPairKind : IO SyntaxNodeKind := nextKind `numPair
 @[init mkNumPairKind] constant numPairKind : SyntaxNodeKind := default _
@@ -33,7 +31,7 @@ node numSetKind $
   "{"; sepBy number ","; "}"
 
 def testParser1 : TermParser :=
-many (numPairP || numSetP)
+many (numPairP <|> numSetP)
 
 def parenIdentP : TermParser :=
 node parenIdentKind $