From 938c8dae83a36f97cefbaf02447b6ea0eadd13ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 26 Sep 2018 09:08:06 -0700 Subject: [PATCH] fix(library/init/control/combinators): `[inline]` ==> `[macro_inline]` --- library/init/control/combinators.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean index 2689318918..14d8b53380 100644 --- a/library/init/control/combinators.lean +++ b/library/init/control/combinators.lean @@ -54,14 +54,14 @@ def list.mforall {m : Type → Type u} [monad m] {α : Type v} (f : α → m boo | [] := pure tt | (a::as) := do b ← f a, if b then list.mforall as else pure ff -@[inline] def when {m : Type → Type u} [monad m] (c : Prop) [h : decidable c] (t : m unit) : m unit := +@[macro_inline] def when {m : Type → Type u} [monad m] (c : Prop) [h : decidable c] (t : m unit) : m unit := if c then t else pure () -@[inline] def unless {m : Type → Type u} [monad m] (c : Prop) [h : decidable c] (e : m unit) : m unit := +@[macro_inline] def unless {m : Type → Type u} [monad m] (c : Prop) [h : decidable c] (e : m unit) : m unit := if c then pure () else e -def mcond {m : Type → Type u} [monad m] {α : Type} (mbool : m bool) (tm fm : m α) : m α := +@[macro_inline] def mcond {m : Type → Type u} [monad m] {α : Type} (mbool : m bool) (tm fm : m α) : m α := do b ← mbool, cond b tm fm -def mwhen {m : Type → Type u} [monad m] (c : m bool) (t : m unit) : m unit := +@[macro_inline] def mwhen {m : Type → Type u} [monad m] (c : m bool) (t : m unit) : m unit := mcond c t (pure ())