Type Definition prop::And

source · [−]

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

Expand description

Logical AND.

Trait Implementations

impl<T: Prop, U: Prop> Commutative<T, U> for And<T, U>

type Out = And<U, T>

The output type for commuted product.

fn commute(self) -> Self::Out

Commutes product.

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

fn decide() -> ExcM<Self>

Get excluded middle rule.

impl<T, U> Product<T, U> for And<T, U>

fn mul(a: T, b: U) -> Self

Creates a product out of two propositions.

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