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),