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

fix: missing comma

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-15 20:29:28 -08:00
parent ed87480093
commit d4ae9e73b1
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

@ -22,13 +22,13 @@ class STWorld (σ : outParam Type) (m : Type → Type)
instance {σ m n} [STWorld σ m] [MonadLift m n] : STWorld σ n := ⟨⟩
instance {ε σ} : STWorld σ (EST ε σ) := ⟨⟩
@[noinline nospecialize]
@[noinline, nospecialize]
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
@[noinline nospecialize]
@[noinline, nospecialize]
def runST {α : Type} (x : forall (σ : Type), ST σ α) : α :=
match x Unit () with
| EStateM.Result.ok a _ => a