Skip to main content

axiom_nonzero_is_not_zero

vstd::std_specs::nonzero

Function axiom_nonzero_is_not_zero 

Source 
pub broadcast proof fn axiom_nonzero_is_not_zero<T: ZeroablePrimitive>(n: NonZero<T>)
Expand description
ensures
!(#[trigger] n@).is_zero(),