lean4-htt/library/init/lean
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
..
ir feat(library/init/control/state): modify monad_run instance for state_t 2018-05-08 17:32:54 -07:00
parser chore(*): remove end after each match-expression 2018-05-04 11:30:06 -07:00
disjoint_set.lean feat(library/init/lean/ir): add elim_phi function 2018-05-06 10:07:44 -07:00
format.lean chore(library/init/lean/ir): improve sizet syntax 2018-05-07 18:07:04 -07:00
name.lean feat(library/init/data/hashable): add hashable nat instance 2018-05-06 07:53:29 -07:00