fact: Fixpoint loc_ids_rlist (l : list nat) (rl : rlist nat ml_int) : M (list nat) := match l with | [::] => Ret [::] | (_ :: t) => match rl with | Nil => Ret [::] | Cons _ r => do rl' <- cget r; do rs <- loc_ids_rlist t rl'; Ret (loc_id r :: rs) end end.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib