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

fix: Parser ==> TrailingParser

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-04 10:07:48 -07:00
parent fa2e943c27
commit 5765a1160d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Parser/Parser.lean
View file

@ -1105,7 +1105,7 @@ checkRbpLt (upper + 1) errorMsg
checkRbpLe prec >> leadingNode n p
/- Version of `trailingNode` which uses `checkRbpLt` -/
@[inline] def trailingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : Parser :=
@[inline] def trailingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : TrailingParser :=
checkRbpLt prec >> trailingNode n p
def mkAtomicInfo (k : String) : ParserInfo :=