diff --git a/src/Lean/Parser/Types.lean b/src/Lean/Parser/Types.lean index fa6a7f83ed..c0e215e6c6 100644 --- a/src/Lean/Parser/Types.lean +++ b/src/Lean/Parser/Types.lean @@ -201,6 +201,7 @@ structure ParserState where namespace ParserState +@[inline] def hasError (s : ParserState) : Bool := s.errorMsg != none