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

chore(library/init/category/state): remove unnecessary assumption

Browse source 
cc @kha
This commit is contained in:
Leonardo de Moura 2018-04-25 17:25:41 -07:00
parent cd4f196842
commit ba47a28dde
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/category/state.lean
View file

@ -105,7 +105,7 @@ instance monad_state_trans {n : Type u → Type w} [has_monad_lift m n] [monad_s
instance [monad m] : monad_state σ (state_t σ m) :=
⟨λ α x, ⟨λ s, pure (x.run s)⟩⟩
variables [monad m] [monad_state σ m]
variables [monad_state σ m]
/-- Obtain the top-most state of a monad stack. -/
@[inline] def get : m σ :=