Function vstd::std_specs::num::ex_u32_checked_rem_euclid
source · pub exec fn ex_u32_checked_rem_euclid(lhs: u32, rhs: u32) -> result : Option<u32>Expand description
ensures
rhs == 0 ==> result.is_None(),rhs != 0 ==> result == Some((lhs % rhs) as u32),