fact: Fixpoint mkrlist (T : ml_type) (l : list (coq_type N T)) (r : loc (ml_rlist T)) : M (loc (ml_rlist T)) := if l is a :: l then do v <- mkrlist T l r; cnew (T:=ml_rlist T) (Cons a v) else Ret r.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib