From 550b5d2b475bf57be42626ac0d490d3150433cfb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Sep 2020 06:54:34 -0700 Subject: [PATCH] chore: missing `[inline]` --- src/Init/System/ST.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean index 0930afb427..6db6e016bf 100644 --- a/src/Init/System/ST.lean +++ b/src/Init/System/ST.lean @@ -21,12 +21,12 @@ class STWorld (σ : outParam Type) (m : Type → Type) instance STWorld.trans {σ m n} [STWorld σ m] [MonadLift m n] : STWorld σ n := ⟨⟩ instance STWorld.base {ε σ} : STWorld σ (EST ε σ) := ⟨⟩ -def runEST {ε α : Type} (x : forall (σ : Type), EST ε σ α) : Except ε α := +@[inline] def runEST {ε α : Type} (x : forall (σ : Type), EST ε σ α) : Except ε α := match x Unit () with | EStateM.Result.ok a _ => Except.ok a | EStateM.Result.error ex _ => Except.error ex -def runST {α : Type} (x : forall (σ : Type), ST σ α) : α := +@[inline] def runST {α : Type} (x : forall (σ : Type), ST σ α) : α := match x Unit () with | EStateM.Result.ok a _ => a | EStateM.Result.error ex _ => Empty.rec _ ex