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