Skip to main content

Module axiom

logicaffeine_compile::ast

Module axiom 

Source
Expand description

AST nodes for the formal-logic vernacular: ## Axiom and ## Theory blocks.

Both store their formal body as RAW TEXT (the same strategy as ProofStrategy::Script, which keeps proof scripts as text for a downstream parser). The formal-formula grammar lives in the proof crate (logicaffeine_proof::formula), so the language crate does not parse it here — it only captures the text, which the compile layer parses into the prover’s ProofExpr.

Structs§

AxiomBlock
A ## Axiom block: a named first-order axiom in formal notation.
TheoryBlock
A ## Theory block: a named development that groups the axioms and theorems that follow it (## Theory Tarski). Its body is the formal development text — a sequence of Axiom … and Theorem … declarations parsed downstream.