Function axiom_has_resolved_entry Copy item path

pub broadcast proof fn axiom_has_resolved_entry<K, V, A: Allocator>(entry: Entry<'_, K, V, A>)

#[trigger] has_resolved(entry) ==> entry.final_value() == entry.value(),