Function vstd::map::axiom_map_empty

pub broadcast proof fn axiom_map_empty<K, V>()

Expand description

ensures

#[trigger] Map::<K, V>::empty().dom() == Set::<K>::empty(),

The domain of the empty map is the empty set

Function vstd::map::axiom_map_emptyCopy item path