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

chore: remove workarounds

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-27 12:40:43 -07:00
parent eabc01d529
commit 573ca7dcad
3 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Command.lean
View file

@ -50,7 +50,7 @@ structure Context :=
(currMacroScope : MacroScope := firstFrontendMacroScope)
(ref : Syntax := Syntax.missing)
abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State (EIO ε)
abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε
abbrev CommandElabM := CommandElabCoreM Exception
abbrev CommandElab := Syntax → CommandElabM Unit
abbrev Linter := Syntax → CommandElabM Unit

2
src/Lean/MetavarContext.lean
View file

@ -594,7 +594,7 @@ def instantiateMVars (mctx : MetavarContext) (e : Expr) : Expr × MetavarContext
if !e.hasMVar then
(e, mctx)
else
let instantiate {ω} (e : Expr) : (MonadCacheT Expr Expr $ StateRefT MetavarContext (ST ω)) Expr :=
let instantiate {ω} (e : Expr) : (MonadCacheT Expr Expr $ StateRefT MetavarContext $ ST ω) Expr :=
instantiateExprMVars e
runST fun _ => instantiate e $.run $.run mctx

4
tests/lean/run/stateRef.lean
View file

@ -39,7 +39,7 @@ instance monadState.hasGetAt (β : Type) (v : β) (α : Type) (m : Type → Type
export HasGetAt (getAt)
abbrev M := StateRefT (Label 0 Nat) (StateRefT (Label 1 Nat) (StateRefT (Label 2 Nat) IO))
abbrev M := StateRefT (Label 0 Nat) $ StateRefT (Label 1 Nat) $ StateRefT (Label 2 Nat) IO
def f4 : M Nat := do
let a0 : Nat ← getAt 0
@ -52,7 +52,7 @@ pure (a0 + a1 + a2)
#eval f4.run' ⟨10⟩ $.run' ⟨20⟩ $.run' ⟨30⟩
abbrev S (ω : Type) := StateRefT Nat (StateRefT String (ST ω))
abbrev S (ω : Type) := StateRefT Nat $ StateRefT String $ ST ω
def f5 {ω} : S ω Unit := do
let s ← getThe String