Type Definition prop::And

pub type And<T, U> = (T, U);

Logical AND.

Trait Implementations

impl<T, U> Decidable for And<T, U>where T: Decidable, U: Decidable,

fn decide() -> ExcM<Self>

Get excluded middle rule.

impl<A: DProp, B: DProp> Existential for And<A, B>

fn e() -> E<Self>

Get existential rule.

impl<A: Prop, X: HLev> HomotopyEquality<A> for And<Eq<Qubit<X, A>, Qubit<X, A>>, <X as HLev>::Out<A, A>>where <X as HLev>::Out<A, A>: HomotopyEquality<A>,

fn refl() -> Self

hom_eq(n, a, a).

impl<A: Prop, B: Prop, X: HLev> HomotopyEquivalence<A, B> for And<Eq<Qubit<X, A>, Qubit<X, B>>, <X as HLev>::Out<A, B>>

type N = S<X>

The associated homotopy level.

type Rel<A2: Prop, B2: Prop> = ((Rc<dyn Fn(Qubit<X, A2>) -> Qubit<X, B2>>, Rc<dyn Fn(Qubit<X, B2>) -> Qubit<X, A2>>), <X as HLev>::Out<A2, B2>)

Relation constructor.

fn transitivity<C: Prop>(self, other: Self::Rel<B, C>) -> Self::Rel<A, C>

hom_eq(n, a, b) ⋀ hom_eq(n, b, c) => hom_eq(n, a, c).

fn symmetry(self) -> Self::Rel<B, A>

hom_eq(n, a, b) => hom_eq(n, b, a).

fn cast<A2: Prop, B2: Prop>(arg: Self) -> Self

Cast to self.

fn cast_lift<A2: Prop, B2: Prop>(self) -> Self

Cast to other.

impl<A, B, T> POrd<T> for And<A, B>where A: POrd<T>, B: POrd<T>,