Type Definition prop::Or

pub type Or<T, U> = Either<T, U>;

Logical OR.

Trait Implementations

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

fn decide() -> ExcM<Self>

Get excluded middle rule.

impl<N: Nat> DecidableHomotopyLevel<N> for Or<True, True>

type H0 = Or<True, True>

A type such that it proves homotopy level 0.

type H = Or<True, True>

A type such that it proves a lower homotopy level.

fn h0<Y: LProp>(ty_y_self: Ty<Y, Self>) -> Q<Self::H0, Y> where
    (N, Z): EqNat, 

Homotopy level 0.

fn hn<X: LProp, Y: LProp>(
    ty_x_self: Ty<X, Self>,
    ty_y_self: Ty<Y, Self>
) -> Q<Self::H, Q<X, Y>> where
    Z: Lt<N>, 

Higher homotopy level.

impl<N: Nat> DecidableHomotopyLevel<N> for Or<True, False>

type H0 = Or<True, False>

A type such that it proves homotopy level 0.

type H = Or<True, False>

A type such that it proves a lower homotopy level.

fn h0<Y: LProp>(ty_y_self: Ty<Y, Self>) -> Q<Self::H0, Y> where
    (N, Z): EqNat, 

Homotopy level 0.

fn hn<X: LProp, Y: LProp>(
    ty_x_self: Ty<X, Self>,
    ty_y_self: Ty<Y, Self>
) -> Q<Self::H, Q<X, Y>> where
    Z: Lt<N>, 

Higher homotopy level.

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