is_partition

vstd_extra::set_extra

Function is_partition 

Source 
pub open spec fn is_partition<A>(s: Set<A>, parts: Set<Set<A>>) -> bool
Expand description
{
    forall |part: Set<A>| {
        #[trigger] parts.contains(part)
            ==> !part.is_empty() && part <= s && pairwise_disjoint(parts)
                && s == parts.flatten()
    }
}