Trait prop::Decidable

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

Implemented by decidable types.

Required Methods

fn decide() -> ExcM<Self>

Get excluded middle rule.

Implementors

impl Decidable for False

impl Decidable for True

impl<A: DProp> Decidable for Pos<A>

impl<A: DProp> Decidable for Qu<A>

impl<A: DProp, B: DProp> Decidable for Pow<A, B>

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

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

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

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

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