Type Definition prop::Imply

pub type Imply<T, U> = Rc<dyn Fn(T) -> U>;

Expand description

Logical IMPLY.

Trait Implementations

impl<T: Prop, U: Prop> Contravariant<Inv<T>, Inv<U>> for Imply<Inv<T>, Inv<U>>

type Out = Inv<Imply<Inv<Inv<U>>, Inv<Inv<T>>>>

The contravariant product type.

fn contra(self) -> Self::Out

Gets the contravariant product.

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

fn decide() -> ExcM<Self>

Get excluded middle rule.

impl<T, U: Prop> Product<T, U> for Imply<T, U>

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

Creates a product out of two propositions.

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