Trait Decidable
prop
pub trait Decidable: Prop { fn decide() -> ExcM<Self>; }
Implemented by decidable types.
fn decide() -> ExcM<Self>
Get excluded middle rule.
impl Decidable for False
fn decide() -> ExcM<False>
impl Decidable for True
fn decide() -> ExcM<True>
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>
fn decide() -> ExcM<POrdProof<T, U>>