Struct Definition 

pub struct Definition {
    pub name: String,
    pub params: Vec<String>,
    pub definiens: ProofExpr,
}

A user-introduced predicate definition (Rung 0a), expressed in the proof layer’s own vocabulary so logicaffeine_proof keeps its no-language-dependency invariant. Read as name(params) :↔ definiens.

Registered as a δ-unfoldable kernel definition (not an inlined expansion), so the definiendum stays a first-class, citable node: bachelor(x) remains bachelor(x) in the proposition, defeq to its meaning by δ-reduction.

Fields

name: String

The definiendum predicate name (e.g. "bachelor").

params: Vec<String>

The parameter names the definiendum binds (e.g. ["x"]).

definiens: ProofExpr

The definiens — the body the definiendum abbreviates.

Trait Implementations

impl Clone for Definition

fn clone(&self) -> Definition

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Definition

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

Formats the value using the given formatter.