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