1      let Monad = ./../Monad/Type
 2  
 3  in  let StateT = ./Type
 4  
 5  in    λ(s : Type)
 6      → λ(m : Type → Type)
 7      → λ(monad : Monad m)
 8      → λ(a : Type)
 9      → λ(state : StateT s m a)
10      → λ(env : s)
11      → monad.bind
12        { val : a, state : s }
13        s
14        (state env)
15        (λ(res : { val : a, state : s }) → monad.pure s res.state)