fact: Fixpoint fib_cps {M : monad} (n : nat) : M nat := match n with | 0 => Ret 1 | 1 => Ret 1 | (m.+1 as sm).+1 => fib_cps sm >>= fun a => fib_cps m >>= fun b => Ret (a + b) end.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib itrace_lib imonad_transformer