max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/parser/parser): notation

Browse source
This commit is contained in:
Leonardo de Moura 2019-06-21 14:20:22 -07:00
parent 43fd0eeb94
commit 0fe8fd1307
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/parser/parser.lean
View file

@ -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 }