Function vstd::std_specs::num::ex_i32_checked_rem_euclid
source · pub exec fn ex_i32_checked_rem_euclid(lhs: i32, rhs: i32) -> result : Option<i32>Expand description
ensures
rhs == 0 ==> result.is_None(),lhs % rhs < i32::MIN || lhs % rhs > i32::MAX ==> result.is_None(),i32::MIN <= lhs % rhs <= i32::MAX ==> result == Some((lhs % rhs) as i32),