Skip to main content

axiom_iset_is_empty

vstd::iset_lib

Function axiom_iset_is_empty 

Source 
pub broadcast proof fn axiom_iset_is_empty<A>(s: ISet<A>)
Expand description
requires
!(#[trigger] s.is_empty()),
ensures
exists |a: A| s.contains(a),