Skip to content

Commit 3cef12a

Browse files
Making this branch work with same Why3 version as main
1 parent 029e3f4 commit 3cef12a

1 file changed

Lines changed: 2 additions & 1 deletion

File tree

theories/distributions/DBool.ec

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,8 @@ lemma dmap_pred (d: 'a distr) (p: 'a -> bool) :
8181
proof.
8282
move => d_ll; apply eq_distr => x.
8383
rewrite dbiased1E clamp_id; first by smt(ge0_mu le1_mu).
84-
rewrite dmap1E /(\o) /pred1; smt(mu_not).
84+
rewrite dmap1E /(\o) /pred1 /=.
85+
by move : (mu_not d p) => /#.
8586
qed.
8687

8788
lemma dbiased1 : dbiased 1%r = dunit true.

0 commit comments

Comments
 (0)