Skip to main content

verify_theorem

logicaffeine_compile::ui_bridge

Function verify_theorem 

Source 
pub fn verify_theorem(input: &str) -> Result<(Term, Context), ParseError>
Expand description

Phase 78: Verify a theorem with full kernel certification.

Pipeline:

  1. Parse theorem block
  2. Extract symbols and build kernel context
  3. Run proof engine
  4. Certify derivation tree to kernel term
  5. Type-check the term
  6. Return (proof_term, context)