Trait prop::quantify::Any

pub trait Any<B: Pred>: Prop {
    fn any<C: Pred>(&self, f: impl All<PImply<B, C>>) -> C;
}

Represents a there-exists quantifier.

Required methods

fn any<C: Pred>(&self, f: impl All<PImply<B, C>>) -> C

∃ x : A { B(x) } <=> ∀ C : P { ∀ x : A { B(x) => C(x) } => C }.

Uses the definition of the existential quantifier from Calculus of Constructions.

Implementors