Trait prop::quantify::Irreflexivity

pub trait Irreflexivity: Pred {
    fn irrefl<A: Prop>(&self) -> Not<Self::Out<And<A, A>>>;
}

Implemented for predicates with an irreflexivity property.

Required methods

fn irrefl<A: Prop>(&self) -> Not<Self::Out<And<A, A>>>

∀ a { ¬p(a, a) }.

Implementors