We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent aa630c4 commit 1a4954eCopy full SHA for 1a4954e
tasks/human_eval_075.rs
@@ -120,7 +120,7 @@ fn is_multiply_prime(x: u32) -> (ans: bool)
120
* k);
121
// prove that that even if the factors are not in the range [2, x], the product is still not equal to x
122
assert forall|i: int, j: int, k: int|
123
- spec_prime(i) && spec_prime(j) && spec_prime(k) ==> x != i * j * k by {
+ spec_prime(i) && spec_prime(j) && spec_prime(k) implies x != i * j * k by {
124
if (i > 1 && j > 1 && k > 1 && (i > x || j > x || k > x)) {
125
broadcast use group_mul_properties;
126
0 commit comments