lean4-htt/library/init/control
Leonardo de Moura 874f9caf13 feat(library/init/control/state): modify monad_run instance for state_t
@Kha, I was having to use `(run ...).1` in many places
in my code. So, I changed the instance
```
instance (σ m out) [monad_run out m] : monad_run (λ α, σ → out (α × σ)) (state_t σ m) :=
⟨λ α x, run ∘ (λ σ, x.run σ)⟩
```
to
```
instance (σ : Type u) (m out : Type u → Type v) [functor m] [monad_run out m] : monad_run (λ α, σ → out α) (state_t σ m) :=
⟨λ α x, run ∘ (λ σ, prod.fst <$> (x.run σ))⟩
```
If we want to get the resultant state in an action `act`, we can just
use `run (act >> get) init_state`.
2018-05-08 17:32:54 -07:00
..
alternative.lean chore(library/init): move logic.lean => core.lean 2018-04-30 09:25:25 -07:00
applicative.lean
combinators.lean feat(library/init/lean/ir): add type checker 2018-05-07 18:07:04 -07:00
default.lean
except.lean feat(library/init/control/except): add monad_except _ except instance 2018-05-08 15:38:20 -07:00
functor.lean refactor(library/init/control): remove init.meta.name spurious dependency 2018-04-30 11:36:07 -07:00
id.lean
lawful.lean
lift.lean
monad.lean
monad_fail.lean
option.lean
reader.lean
state.lean feat(library/init/control/state): modify monad_run instance for state_t 2018-05-08 17:32:54 -07:00