Function axiom_structural_obeys_concrete_eq

pub broadcast proof fn axiom_structural_obeys_concrete_eq<T: PartialEq + Structural>()

Expand description

requires

T::obeys_eq_spec(),

forall |x: T, y: T| x.eq_spec(&y) <==> x == y,

ensures

#[trigger] obeys_concrete_eq::<T>(),

Function axiom_structural_obeys_concrete_eqCopy item path