fact: Definition omap (a : K * V -> option V') f : U' := if valid f then foldl (fun z kv => if a kv is Some v' then z \+ pts kv.1 v' else z) Unit (assocs f) else undef.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)