fact: Fixpoint evalDist(A : Set)(c : Comp A) : Distribution A := match c with | Ret eqd a => fun a' => if (eqd a a') then 1 else 0 | Bind c1 c2 => fun a => sumList (getSupport c1) (fun b => (evalDist c1 b) * (evalDist (c2 b) a)) | Rnd n => fun v => 1 / (expnat 2 n) | Repeat c P => fun a => (indicator P a) * (ratInverse (sumList (filter P (getSupport c)) (evalDist c))) * (evalDist c a) end.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec