Variable bernoulli : R -> O bool. let binomial (p:R) : nat -> O nat := let berp : O bool := bernoulli p in fix binp (n:nat) variant "Lt" : O nat := if (n = Zero) then prob Zero else prob sample x from binp (Pred n) in sample b from berp in if b then Succ x else x .