Enum ProofExpr 

pub enum ProofExpr {
    Predicate {
        name: String,
        args: Vec<ProofTerm>,
        world: Option<String>,
    },
    Identity(ProofTerm, ProofTerm),
    Atom(String),
    And(Box<ProofExpr>, Box<ProofExpr>),
    Or(Box<ProofExpr>, Box<ProofExpr>),
    Implies(Box<ProofExpr>, Box<ProofExpr>),
    Iff(Box<ProofExpr>, Box<ProofExpr>),
    Not(Box<ProofExpr>),
    ForAll {
        variable: String,
        body: Box<ProofExpr>,
    },
    Exists {
        variable: String,
        body: Box<ProofExpr>,
    },
    Modal {
        domain: String,
        force: f32,
        flavor: String,
        body: Box<ProofExpr>,
    },
    Temporal {
        operator: String,
        body: Box<ProofExpr>,
    },
    Lambda {
        variable: String,
        body: Box<ProofExpr>,
    },
    App(Box<ProofExpr>, Box<ProofExpr>),
    NeoEvent {
        event_var: String,
        verb: String,
        roles: Vec<(String, ProofTerm)>,
    },
    Ctor {
        name: String,
        args: Vec<ProofExpr>,
    },
    Match {
        scrutinee: Box<ProofExpr>,
        arms: Vec<MatchArm>,
    },
    Fixpoint {
        name: String,
        body: Box<ProofExpr>,
    },
    TypedVar {
        name: String,
        typename: String,
    },
    Hole(String),
    Term(ProofTerm),
    Unsupported(String),
}

Owned expression representation for proof manipulation.

Supports all LogicExpr variants to enable full language coverage. This is the “proposition” side of the Curry-Howard correspondence.

See Also

• ProofTerm - Terms embedded within expressions (predicate arguments)
• unify::unify_exprs - Expression-level unification with alpha-equivalence
• unify::beta_reduce - Normalizes lambda applications
• certifier::certify - Converts expressions to kernel types
• DerivationTree - Proof trees conclude with a ProofExpr

Variants

Predicate

Atomic predicate: P(t1, t2, …)

Fields

name: String

args: Vec<ProofTerm>

world: Option<String>

Identity(ProofTerm, ProofTerm)

Identity: t1 = t2

Atom(String)

Propositional atom

And(Box<ProofExpr>, Box<ProofExpr>)

Conjunction: P ∧ Q

Or(Box<ProofExpr>, Box<ProofExpr>)

Disjunction: P ∨ Q

Implies(Box<ProofExpr>, Box<ProofExpr>)

Implication: P → Q

Iff(Box<ProofExpr>, Box<ProofExpr>)

Biconditional: P ↔ Q

Not(Box<ProofExpr>)

Negation: ¬P

ForAll

Universal quantification: ∀x P(x)

Fields

variable: String

body: Box<ProofExpr>

Exists

Existential quantification: ∃x P(x)

Fields

variable: String

body: Box<ProofExpr>

Modal

Modal operator: □P or ◇P (with world semantics)

Fields

domain: String

force: f32

flavor: String

body: Box<ProofExpr>

Temporal

Temporal operator: Past(P) or Future(P)

Fields

operator: String

body: Box<ProofExpr>

Lambda

Lambda abstraction: λx.P

Fields

variable: String

body: Box<ProofExpr>

App(Box<ProofExpr>, Box<ProofExpr>)

Function application: (f x)

NeoEvent

Neo-Davidsonian event: ∃e(Verb(e) ∧ Agent(e,x) ∧ …)

Fields

event_var: String

verb: String

roles: Vec<(String, ProofTerm)>

Ctor

Data Constructor: Zero, Succ(n), Cons(h, t), etc. The building blocks of inductive types.

Fields

name: String

args: Vec<ProofExpr>

Match

Pattern Matching: match n { Zero => A, Succ(k) => B } Eliminates inductive types by case analysis.

Fields

scrutinee: Box<ProofExpr>

arms: Vec<MatchArm>

Fixpoint

Recursive Function (Fixpoint): fix f. λn. … Defines recursive functions over inductive types.

Fields

name: String

body: Box<ProofExpr>

TypedVar

Typed Variable: n : Nat Signals to the prover that induction may be applicable.

Fields

name: String

typename: String

Hole(String)

Meta-variable (unification hole) to be solved during proof search. Represents an unknown expression, typically a function or predicate. Example: Hole(“P”) in ?P(x) = Body, to be solved as P = λx.Body

Term(ProofTerm)

Embedded term (lifts ProofTerm into ProofExpr context). Used when a term appears where an expression is expected. Example: App(Hole(“P”), Term(BoundVarRef(“x”)))

Unsupported(String)

Unsupported construct (with description for debugging)

Trait Implementations

impl Clone for ProofExpr

fn clone(&self) -> ProofExpr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofExpr

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

Formats the value using the given formatter.

impl Display for ProofExpr

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

Formats the value using the given formatter.

impl PartialEq for ProofExpr

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