Module State

Meta-data

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..∞])

[top] Functor

fmap_state : forall {a : Type, b : Type, s : Type} 
           . (a -> b) -> State s a -> State s b

[top] Monad

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