pub fn compile_theory_for_ui(input: &str) -> TheoryCompileResultExpand description
Compile a program’s formal development end to end: collect every ## Axiom (a shared
premise base) and every ## Theory block’s Axiom/Theorem declarations, then prove
the theorems in citation order, each kernel-certified by the multi-theorem driver. This
is the seam that turns a Tarski-style source file into a verified development.