fact: Fixpoint fibo_ref n (a b : loc ml_int) : M unit := if n is n.+1 then cget a >>= (fun x => cget b >>= fun y => cput a y >> cput b (x + y)) >> fibo_ref n a b else skip.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib