Function vstd::std_specs::num::ex_u32_checked_rem

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