fact: Fixpoint Run_aux {A : choiceType} (c : raw_code A) (seed : nat) (st : Location → option NatState) : option A := match c with ret x => Some x | sampler o k => match sample (projT1 o) seed with | Some (seed', x) => Run_aux (k x) seed' st | _ => None end | opr o x k => None | putr l v k => Run_aux k seed (new_state st l v) | getr l k => match nat_ch (st l) l with | Some v => Run_aux (k v) seed st | None => None end end.
imports: mathcomp(all_ssreflect) Crypt(Prelude choice_type pkg_core_definition pkg_tactics pkg_distr pkg_notation) Coq(Utf8) extructures(ord fset fmap) Equations(Equations)