Contents
[top] State data type, constructor and deconstructors
data State (s : Type) (a : Type) where
State (s [0..∞] -> (a, s [0..∞]))
runState : forall {a : Type, s : Type}
. State s a -> s [0..∞] -> (a, s [0..∞])
fmap_state : forall {a : Type, b : Type, s : Type}
. (a -> b) -> State s a -> State s b
return_state : forall {a : Type, s : Type}
. a -> State s a
bind_state : forall {a : Type, b : Type, s : Type}
. (a -> State s b) -> State s a -> State s b
join_state : forall {a : Type, b : Type, s : Type}
. State s (State s a) -> State s a