logicaffeine_language/ast/
axiom.rs

1//! AST nodes for the formal-logic vernacular: `## Axiom` and `## Theory` blocks.
2//!
3//! Both store their formal body as RAW TEXT (the same strategy as
4//! [`ProofStrategy::Script`](super::theorem::ProofStrategy), which keeps proof scripts as
5//! text for a downstream parser). The formal-formula grammar lives in the proof crate
6//! (`logicaffeine_proof::formula`), so the language crate does not parse it here — it only
7//! captures the text, which the compile layer parses into the prover's `ProofExpr`.
8
9/// A `## Axiom` block: a named first-order axiom in formal notation.
10///
11/// `## Axiom flip: for all a b, Cong(a, b, b, a).` registers `flip` as a shared premise
12/// available to every later theorem in the program — the seam for an axiomatic base like
13/// Tarski geometry.
14#[derive(Debug, Clone, PartialEq, Eq)]
15pub struct AxiomBlock {
16    /// The axiom's name (`flip`), for citation and diagnostics.
17    pub name: String,
18    /// The axiom formula as surface text, parsed downstream by the formal-formula parser.
19    pub formula: String,
20}
21
22/// A `## Theory` block: a named development that groups the axioms and theorems that
23/// follow it (`## Theory Tarski`). Its body is the formal development text — a sequence of
24/// `Axiom …` and `Theorem …` declarations parsed downstream.
25#[derive(Debug, Clone, PartialEq, Eq)]
26pub struct TheoryBlock {
27    /// The theory's name (`Tarski`).
28    pub name: String,
29    /// The development body as surface text: `Axiom …` / `Theorem …` declarations, parsed
30    /// downstream by the formal-development parser. Empty when the theory is just a header
31    /// grouping standalone `## Axiom` / `## Theorem` blocks.
32    pub body: String,
33}
logicaffeine_language/ast/axiom.rs

logicaffeine_language/ast/
axiom.rs
