fix(init/category/state): lift unintended universe restriction

This commit is contained in:
Sebastian Ullrich 2018-03-26 13:00:23 +02:00
parent 06e0d78e21
commit a41d797900

View file

@ -95,7 +95,7 @@ class monad_state (σ : out_param (Type u)) (m : Type u → Type v) :=
(lift {} {α : Type u} : state σ α → m α)
section
variables {σ : Type u} {m : Type u → Type u}
variables {σ : Type u} {m : Type u → Type v}
-- NOTE: The ordering of the following two instances determines that the top-most `state_t` monad layer
-- will be picked first