From 0fe8fd130754fc43ca8d39255ee1bbb6c7a87034 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 21 Jun 2019 14:20:22 -0700
Subject: [PATCH] feat(library/init/lean/parser/parser): notation

---
 library/init/lean/parser/parser.lean | 6 ++++++
 1 file changed, 6 insertions(+)

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 }