Trait prop::Decidable[−][src]

pub trait Decidable: Prop {
    fn decide() -> ExcM<Self>;
}

Implemented by decidable types.

Required methods

fn decide() -> ExcM<Self>[src]

Get excluded middle rule.

Loading content...

Implementors

impl Decidable for False[src]

fn decide() -> ExcM<False>[src]

impl Decidable for True[src]

fn decide() -> ExcM<True>[src]

impl<N: 'static + Default + Clone> Decidable for LTrue<N>[src]

fn decide() -> ExcM<Self>[src]

impl<T, U> Decidable for And<T, U> where
    T: Decidable,
    U: Decidable, [src]

fn decide() -> ExcM<Self>[src]

impl<T, U> Decidable for Imply<T, U> where
    T: Decidable,
    U: Decidable, [src]

fn decide() -> ExcM<Self>[src]

impl<T, U> Decidable for Or<T, U> where
    T: Decidable,
    U: Decidable, [src]

fn decide() -> ExcM<Self>[src]

impl<T: 'static, U: 'static> Decidable for POrdProof<T, U>[src]

fn decide() -> ExcM<POrdProof<T, U>>[src]

Loading content...