Function vstd::std_specs::num::ex_i32_checked_div_euclid

source · 
pub exec fn ex_i32_checked_div_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),