Enum ProofTerm 

pub enum ProofTerm {
    Constant(String),
    Variable(String),
    Function(String, Vec<ProofTerm>),
    Group(Vec<ProofTerm>),
    BoundVarRef(String),
}

Owned term representation for proof manipulation.

Decoupled from arena-allocated Term<'a> to allow proof trees to persist beyond the lifetime of the parsing arena.

See Also

• ProofExpr - Expression-level representation containing ProofTerms
• unify::unify_terms - Unification algorithm for terms
• unify::Substitution - Maps variables to terms
• certifier::certify - Converts proof trees to kernel terms

Variants

Constant(String)

A constant symbol (e.g., “Socrates”, “42”)

Variable(String)

A variable symbol (e.g., “x”, “y”)

Function(String, Vec<ProofTerm>)

A function application (e.g., “father(x)”, “add(1, 2)”)

Group(Vec<ProofTerm>)

A group/tuple of terms (e.g., “(x, y)”)

BoundVarRef(String)

Reference to a bound variable in a pattern context. Distinct from Variable (unification var) and Constant (global name). Prevents variable capture bugs during alpha-conversion.

Trait Implementations

impl Clone for ProofTerm

fn clone(&self) -> ProofTerm

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofTerm

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

Formats the value using the given formatter.

impl Display for ProofTerm

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

Formats the value using the given formatter.

impl Hash for ProofTerm

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 ProofTerm

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

impl StructuralPartialEq for ProofTerm