Enum TermProof 

pub enum TermProof {
    PRule {
        rule_name: Rc<str>,
        subst: DenseIdMap<VariableId, TermId>,
        body_pfs: Vec<Premise>,
        result: TermId,
    },
    PProj {
        pf_f_args_ok: TermProofId,
        arg_idx: usize,
    },
    PCong(CongProof),
    PFiat {
        desc: Rc<str>,
        term: TermId,
    },
}

Variants

PRule

proves a Proposition based on a rule application the subsitution gives the mapping from variables to terms the body_pfs gives proofs for each of the conditions in the query of the rule the act_pf gives a location in the action of the proposition

Fields

rule_name: Rc<str>

subst: DenseIdMap<VariableId, TermId>

body_pfs: Vec<Premise>

result: TermId

PProj

get a proof for the child of a term given a proof of a term

Fields

pf_f_args_ok: TermProofId

arg_idx: usize

PCong(CongProof)

PFiat

Fields

desc: Rc<str>

term: TermId

Trait Implementations

impl Clone for TermProof

fn clone(&self) -> TermProof

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TermProof

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Hash for TermProof

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for TermProof

fn eq(&self, other: &TermProof) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for TermProof

impl StructuralPartialEq for TermProof