fact: Definition bind {A B : UU0} (m : failPState A) (f : A -> failPState B) : failPState B := fun s => match m s with | (None, s') => (None, s') | (Some a, s') => f a s' end.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib monad_transformer