Enum cop::lean::Proof

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

A full proof for a literal, including subproofs.

Variants

Lem

Lemma step

Red

Reduction step

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

Extension step, storing proofs for all items of the contrapositive

Implementations

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

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

Produce a tree-like proof from a series of proof search actions.

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

Given a proof and the literal it proves, make it into something that can be displayed.

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

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

Check the proof.