diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean index fbcf7e433d..87cfda4640 100644 --- a/library/init/lean/parser/parsec.lean +++ b/library/init/lean/parser/parsec.lean @@ -91,7 +91,7 @@ protected def failure : parsec_t μ m α := def merge (msg₁ msg₂ : message μ) : message μ := { expected := msg₁.expected ++ msg₂.expected, ..msg₁ } -@[inline] private def bind_mk_res (ex₁ : option (dlist string)) (r : result μ β) : result μ β := +@[inline_if_reduce] private def bind_mk_res (ex₁ : option (dlist string)) (r : result μ β) : result μ β := match ex₁, r with | none, ok b it _ := ok b it none | none, error msg _ := error msg tt @@ -148,6 +148,7 @@ match r with r ← p it, pure $ labels_mk_res r lbls +@[inline_if_reduce] private def try_mk_res (r : result μ α) : result μ α := match r with | error msg _ := error msg ff @@ -175,7 +176,7 @@ Without the `try` combinator we will not be able to backtrack on the `let` keywo r ← p it, pure $ try_mk_res r -@[inline] private def orelse_mk_res (msg₁ : message μ) (r : result μ α) : result μ α := +@[inline_if_reduce] private def orelse_mk_res (msg₁ : message μ) (r : result μ α) : result μ α := match r with | ok a it' (some ex₂) := ok a it' (some $ msg₁.expected ++ ex₂) | error msg₂ ff := error (merge msg₁ msg₂) ff