diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean index 0876df33d6..23071ae7c6 100644 --- a/src/Lean/Parser/Parser.lean +++ b/src/Lean/Parser/Parser.lean @@ -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 :=