max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: missing [inline]

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-24 06:54:34 -07:00
parent f73fca1da7
commit 550b5d2b47
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/System/ST.lean
View file

@ -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