From b4b42ef8b2ecac681bfcbd900cf92090c87315c1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 24 Sep 2018 18:57:49 -0700 Subject: [PATCH] feat(library/init/lean/parser/parsec): missing `[inline]` --- library/init/lean/parser/parsec.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean index 53be0114ba..6231e179c1 100644 --- a/library/init/lean/parser/parsec.lean +++ b/library/init/lean/parser/parsec.lean @@ -168,7 +168,7 @@ together. ``` Without the `try` combinator we will not be able to backtrack on the `let` keyword. -/ -def try (p : parsec_t μ m α) : parsec_t μ m α := +@[inline] def try (p : parsec_t μ m α) : parsec_t μ m α := λ it, do r ← p it, pure $ match r with @@ -187,7 +187,7 @@ def try (p : parsec_t μ m α) : parsec_t μ m α := combine their error messages (even if one of them succeeded). -/ -protected def orelse (p q : parsec_t μ m α) : parsec_t μ m α := +@[inline] protected def orelse (p q : parsec_t μ m α) : parsec_t μ m α := λ it, do r ← p it, match r with