Skip to main content

full_set_properties

Function full_set_properties 

Source
pub broadcast proof fn full_set_properties<A: FiniteFull>()
Expand description
ensures
Set::<A>::full() is Some,

This public broadcast lemma shows that when A has trait FiniteRange, A::full() has the expected propery of containing all values of type A.