fact: Definition forloop63 (n_1 n_2 : int) (b : int -> M unit) : M unit := if Sint63.ltb n_2 n_1 then Ret tt else iter (uint2N (sub n_2 n_1)).+1 (fun (m : M int) => do i <- m; do _ <- b i; Ret (Uint63.succ i)) (Ret n_1) >> Ret tt.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63