Skip to main content

axiom_view_nonzero_from_primitive_eq

vstd::std_specs::nonzero

Function axiom_view_nonzero_from_primitive_eq 

Source 
pub broadcast proof fn axiom_view_nonzero_from_primitive_eq<T: ZeroablePrimitive>(n: NonZero<T>)
Expand description
ensures
#[trigger] nonzero_from_primitive(n@) == n,