Enum EqProof 

pub enum EqProof {
    PRule {
        rule_name: Rc<str>,
        subst: DenseIdMap<VariableId, TermId>,
        body_pfs: Vec<Premise>,
        result_lhs: TermId,
        result_rhs: TermId,
    },
    PRefl {
        t_ok_pf: TermProofId,
        t: TermId,
    },
    PSym {
        eq_pf: EqProofId,
    },
    PTrans {
        pfxy: EqProofId,
        pfyz: EqProofId,
    },
    PCong(CongProof),
}

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_lhs: TermId

result_rhs: TermId

PRefl

A term is equal to itself- proves the proposition t = t

Fields

t_ok_pf: TermProofId

t: TermId

PSym

The symmetric equality of eq_pf

Fields

eq_pf: EqProofId

PTrans

Fields

pfxy: EqProofId

pfyz: EqProofId

PCong(CongProof)

Proves f(x1, y1, …) = f(x2, y2, …) where f is fun_sym A proof via congruence- one proof for each child of the term pf_f_args_ok is a proof that the term with the lhs children is valid

Trait Implementations

impl Clone for EqProof

fn clone(&self) -> EqProof

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for EqProof

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

Formats the value using the given formatter.

impl Hash for EqProof

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 EqProof

fn eq(&self, other: &EqProof) -> 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 EqProof

impl StructuralPartialEq for EqProof