Skip to content

Commit e8ac050

Browse files
kani::forall -> forall
1 parent 0ff0c95 commit e8ac050

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

library/core/src/num/dec2flt/decimal_seq.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -141,7 +141,7 @@ impl DecimalSeq {
141141
n < 10u64 << (shift - 1) &&
142142
self.num_digits <= Self::MAX_DIGITS &&
143143
self.decimal_point <= self.num_digits as i32 &&
144-
kani::forall!(|i in (0,DecimalSeq::MAX_DIGITS)| self.digits[i] <= 9)
144+
forall!(|i in (0,DecimalSeq::MAX_DIGITS)| self.digits[i] <= 9)
145145
)]
146146
while read_index != 0 {
147147
read_index -= 1;
@@ -414,7 +414,7 @@ pub mod decimal_seq_verify {
414414
digits: kani::any(),
415415
};
416416
kani::assume(ret.decimal_point <= ret.num_digits as i32);
417-
kani::assume(kani::forall!(|i in (0,DecimalSeq::MAX_DIGITS)| ret.digits[i] <= 9));
417+
kani::assume(forall!(|i in (0,DecimalSeq::MAX_DIGITS)| ret.digits[i] <= 9));
418418
ret
419419
}
420420
}

0 commit comments

Comments
 (0)