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-08-23 19:54:58 -07:00
parent 6fc935f6d1
commit b672f0820b
3 changed files with 3 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/LeanInit.lean
View file

@ -147,15 +147,10 @@ let r := ngen.curr;
setNGen ngen.next;
pure r
-- TODO: mark as instance as soon as we move to new frontend
def monadNameGeneratorLift (m : Type → Type) {n : Type → Type} [MonadNameGenerator m] [HasMonadLiftT m n] : MonadNameGenerator n :=
instance monadNameGeneratorLift (m n : Type → Type) [MonadNameGenerator m] [HasMonadLift m n] : MonadNameGenerator n :=
{ getNGen := liftM (getNGen : m _),
setNGen := fun ngen => liftM (setNGen ngen : m _) }
instance ReaderT.monadNGen {m ρ} [Monad m] [MonadNameGenerator m] : MonadNameGenerator (ReaderT ρ m) := monadNameGeneratorLift m
instance StateRefT.monadNGen {ω m σ} [MonadNameGenerator m] : MonadNameGenerator (StateRefT' ω σ m) := monadNameGeneratorLift m
instance OptionT.monadNGen {m} [Monad m] [MonadNameGenerator m] : MonadNameGenerator (OptionT m) := monadNameGeneratorLift m
/-
Small DSL for describing parsers. We implement an interpreter for it
at `Parser.lean` -/

6
src/Lean/Data/Options.lean
View file

@ -95,13 +95,9 @@ class MonadOptions (m : Type → Type) :=
export MonadOptions (getOptions)
/- We currently cannot mark the following definition as an instance since it increases the search space too much -/
def monadOptsFromLift (m) {n} [MonadOptions m] [HasMonadLiftT m n] : MonadOptions n :=
instance monadOptsFromLift (m n) [MonadOptions m] [HasMonadLift m n] : MonadOptions n :=
{ getOptions := liftM (getOptions : m _) }
instance ReaderT.monadOpts {ρ m} [MonadOptions m] : MonadOptions (ReaderT ρ m) := monadOptsFromLift m
instance StateRefT.monadOpts {ω σ m} [MonadOptions m] : MonadOptions (StateRefT' ω σ m) := monadOptsFromLift m
section Methods
variables {m : Type → Type} [Monad m] [MonadOptions m]

7
src/Lean/MonadEnv.lean
View file

@ -15,15 +15,10 @@ class MonadEnv (m : Type → Type) :=
export MonadEnv (getEnv modifyEnv)
/- We currently cannot mark the following definition as an instance since it increases the search space too much -/
def monadEnvFromLift (m) {n} [MonadEnv m] [HasMonadLiftT m n] : MonadEnv n :=
instance monadEnvFromLift (m n) [MonadEnv m] [HasMonadLift m n] : MonadEnv n :=
{ getEnv := liftM (getEnv : m Environment),
modifyEnv := fun f => liftM (modifyEnv f : m Unit) }
instance ReaderT.monadEnv {m ρ} [Monad m] [MonadEnv m] : MonadEnv (ReaderT ρ m) := monadEnvFromLift m
instance StateRefT.monadEnv {ω m σ} [MonadEnv m] : MonadEnv (StateRefT' ω σ m) := monadEnvFromLift m
instance OptionT.monadEnv {m} [Monad m] [MonadEnv m] : MonadEnv (OptionT m) := monadEnvFromLift m
section Methods
variables {m : Type → Type} [MonadEnv m]