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 $