diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 2b148741bb..080858ea1e 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -202,6 +202,9 @@ abbrev TrailingParser := Parser trailing { info := andthenInfo p.info q.info, fn := andthenFn p.fn q.fn } +instance hashAndthen {k : ParserKind} : HasAndthen (Parser k) := +⟨andthen⟩ + @[inline] def nodeFn {k : ParserKind} (n : SyntaxNodeKind) (p : ParserFn k) : ParserFn k | a c s := let iniSz := s.stackSize in @@ -231,6 +234,9 @@ abbrev TrailingParser := Parser trailing { info := orelseInfo p.info q.info, fn := orelseFn p.fn q.fn } +instance hashOrelse {k : ParserKind} : HasOrelse (Parser k) := +⟨orelse⟩ + @[noinline] def noFirstTokenInfo (info : ParserInfo) : ParserInfo := { updateTokens := info.updateTokens }