inner_state.lean

universes u v w

class monad_state' (σ : Type u) (m : Type u → Type v) :=
(lift {} {α : Type u} : state σ α → m α)

section
variables {σ : Type u} {m : Type u → Type v}

instance ss' [s : monad_state σ m] : monad_state' σ m :=
{lift := @monad_state.lift _ _ _}

@[inline] def get' (σ : Type u) {m : Type u → Type v} [monad m] [monad_state' σ m] : m σ :=
monad_state'.lift state_t.get

end

def bistate_test : state_t ℕ (state_t bool io) unit :=
do 0  ← get,       -- outer state_t wins
   tt ← get' bool, -- use the type to select the inner state
   pure ()