Trait prop::Decidable

pub trait Decidable: Prop {
    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<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>