logicaffeine-language 0.10.1

Natural language to first-order logic pipeline
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

//! `## Define` block AST — a vernacular-logic predicate definition (Rung 0a).
//!
//! A definition introduces a new predicate (the *definiendum*) as an
//! abbreviation for a formula over its parameters (the *definiens*), written as
//! a biconditional sentence:
//!
//! ```text
//! ## Define
//! x is a bachelor if and only if x is unmarried and x is a man.
//! ```
//!
//! The parser splits the biconditional: the LHS `Predicate` supplies the
//! definiendum name and its parameter symbols; the RHS is the definiens. The
//! proof layer registers this as a δ-unfoldable kernel definition, so the
//! predicate becomes a reusable, citable node — not an inlined expansion.

use super::logic::LogicExpr;
use logicaffeine_base::Symbol;

/// A `## Define` block: `<definiendum>(params) if and only if <definiens>`.
#[derive(Debug, Clone)]
pub struct DefinitionBlock<'a> {
    /// The definiendum predicate name (the LHS predicate, e.g. `"bachelor"`).
    pub name: String,
    /// The parameter symbols the definiendum binds (its LHS arguments).
    pub params: Vec<Symbol>,
    /// The definiendum application — the LHS `Predicate` of the biconditional.
    pub definiendum: &'a LogicExpr<'a>,
    /// The definiens — the RHS of the biconditional.
    pub definiens: &'a LogicExpr<'a>,
}