logicaffeine_language/ast/
definition.rs

1//! `## Define` block AST — a vernacular-logic predicate definition (Rung 0a).
2//!
3//! A definition introduces a new predicate (the *definiendum*) as an
4//! abbreviation for a formula over its parameters (the *definiens*), written as
5//! a biconditional sentence:
6//!
7//! ```text
8//! ## Define
9//! x is a bachelor if and only if x is unmarried and x is a man.
10//! ```
11//!
12//! The parser splits the biconditional: the LHS `Predicate` supplies the
13//! definiendum name and its parameter symbols; the RHS is the definiens. The
14//! proof layer registers this as a δ-unfoldable kernel definition, so the
15//! predicate becomes a reusable, citable node — not an inlined expansion.
16
17use super::logic::LogicExpr;
18use logicaffeine_base::Symbol;
19
20/// A `## Define` block: `<definiendum>(params) if and only if <definiens>`.
21#[derive(Debug, Clone)]
22pub struct DefinitionBlock<'a> {
23    /// The definiendum predicate name (the LHS predicate, e.g. `"bachelor"`).
24    pub name: String,
25    /// The parameter symbols the definiendum binds (its LHS arguments).
26    pub params: Vec<Symbol>,
27    /// The definiendum application — the LHS `Predicate` of the biconditional.
28    pub definiendum: &'a LogicExpr<'a>,
29    /// The definiens — the RHS of the biconditional.
30    pub definiens: &'a LogicExpr<'a>,
31}
logicaffeine_language/ast/definition.rs

logicaffeine_language/ast/
definition.rs
