From aab0e382c8024ae27ccaf5d5b8d6a300507b473d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 17 Aug 2023 10:47:23 +0200 Subject: [PATCH] perf: inline ParserState.hasError --- src/Lean/Parser/Types.lean | 1 + 1 file changed, 1 insertion(+) 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