WIP: add_RV_unif type issue

affeldt-aist · Jan 6, 2025 · b7c2583 · b7c2583
1 parent fa397f0
commit b7c2583
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/probability/smc.v b/probability/smc.v
@@ -162,7 +162,7 @@ Variable n : nat.
 Variables (X Y : {RV P -> A}).
 
 (* How to express "the distribution of random variable Y is uniform distribution" as a prop. *)
-Hypothesis card_A : #|A| = n.+1.
+Hypothesis card_A : #|A:finType| = n.+1.
 Variable pY_unif : `p_ Y = fdist_uniform card_A.
 Variable XY_indep : P |= X _|_ Y.