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

fix(init/category/transformers): make has_monad_lift more universe polymorphic

Browse source
This commit is contained in:
Sebastian Ullrich 2018-01-06 00:56:46 +01:00 • committed by Leonardo de Moura
parent 1a0363c7c2
commit 248e035402
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/category/transformers.lean
View file

@ -16,13 +16,13 @@ class monad_transformer (transformer : ∀ (m : Type u → Type v) [monad m], Ty
instance transformed_monad (m t) [monad_transformer t] [monad m] : monad (t m) :=
monad_transformer.is_monad t m
class has_monad_lift (m n : Type u → Type v) :=
class has_monad_lift (m : Type u → Type v) (n : Type u → Type w) :=
(monad_lift : ∀ α, m α → n α)
instance monad_transformer_lift (t m) [monad_transformer t] [monad m] : has_monad_lift m (t m) :=
⟨monad_transformer.monad_lift t m⟩
class has_monad_lift_t (m n : Type u → Type v) :=
class has_monad_lift_t (m : Type u → Type v) (n : Type u → Type w) :=
(monad_lift : ∀ α, m α → n α)
def monad_lift {m n} [has_monad_lift_t m n] {α} : m α → n α :=