fact: Definition randomFunc (f : (list (D * R))) (d : D) : Comp (R * list (D * R)) := match (arrayLookup _ f d) with | None => (r <-$ RndR; ret (r, (d, r) :: f)) | Some r => ret (r, f) end.
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid