Enum cop::lean::Proof[][src]

pub enum Proof<'t, P, C> {
    Lem,
    Red,
    Ext(Offset<&'t Contrapositive<P, C, usize>>, Vec<Self>),
}

Variants

Lem
Red
Ext(Offset<&'t Contrapositive<P, C, usize>>, Vec<Self>)

Implementations

impl<'t, P, C> Proof<'t, P, C>[src]

pub fn from_iter(
    iter: &mut impl Iterator<Item = Action<'t, P, C>>,
    off: &mut usize
) -> Self
[src]

pub fn display(&self, lit: OLit<'t, P, C>) -> Disp<'_, 't, P, C>[src]

impl<'t, P: Eq + Neg<Output = P> + Clone, C: Eq> Proof<'t, P, C>[src]

pub fn check(
    &self,
    sub: &Sub<'t, C>,
    lit: OLit<'t, P, C>,
    ctx: Context<'t, P, C>
) -> bool
[src]

Auto Trait Implementations

impl<'t, P, C> RefUnwindSafe for Proof<'t, P, C> where
    C: RefUnwindSafe,
    P: RefUnwindSafe

impl<'t, P, C> Send for Proof<'t, P, C> where
    C: Sync,
    P: Sync

impl<'t, P, C> Sync for Proof<'t, P, C> where
    C: Sync,
    P: Sync

impl<'t, P, C> Unpin for Proof<'t, P, C>

impl<'t, P, C> UnwindSafe for Proof<'t, P, C> where
    C: RefUnwindSafe,
    P: RefUnwindSafe

Blanket Implementations

impl<T> Any for T where
    T: 'static + ?Sized
[src]

impl<T> Borrow<T> for T where
    T: ?Sized
[src]

impl<T> BorrowMut<T> for T where
    T: ?Sized
[src]

impl<T> From<T> for T[src]

impl<T, U> Into<U> for T where
    U: From<T>, 
[src]

impl<T, U> TryFrom<U> for T where
    U: Into<T>, 
[src]

type Error = Infallible

The type returned in the event of a conversion error.

impl<T, U> TryInto<U> for T where
    U: TryFrom<T>, 
[src]

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.