From 370f67b27bd5880fe35fe4aab800e9e223ade8dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 25 Oct 2018 10:10:54 -0700
Subject: [PATCH] feat(library/init/lean/parser/parsec): mark `*_mk_res`
 functions as `[inline_if_reduce]`

---
 library/init/lean/parser/parsec.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

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