Add comment

tautschnig · tautschnig · commit f67539e8ab84 · 2025-05-30T09:54:38.000Z
diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs
@@ -2606,6 +2606,7 @@ mod verify {
         };
     }
 
+    // Use for NonZero what already worked well for general numeric types (see num/mod.rs)
     macro_rules! check_mul_unchecked_intervals {
         ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => {
             #[kani::proof_for_contract(NonZero::<$t>::unchecked_mul)]

Original file line number	Diff line number	Diff line change
`@@ -2606,6 +2606,7 @@ mod verify {`
`2606`	`2606`	`};`
`2607`	`2607`	`}`
`2608`	`2608`
	`2609`	`+ // Use for NonZero what already worked well for general numeric types (see num/mod.rs)`
`2609`	`2610`	`macro_rules! check_mul_unchecked_intervals {`
`2610`	`2611`	`($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => {`
`2611`	`2612`	`#[kani::proof_for_contract(NonZero::<$t>::unchecked_mul)]`