Skip to main content

prove_development

Function prove_development 

Source
pub fn prove_development(
    body: &str,
) -> Result<Vec<(String, LibraryResult)>, FormulaError>
Expand description

Parse a ## Theory body and discharge every theorem against the development’s axioms (and cited lemmas), in citation order — each kernel-certified. Results are in source order, paired with the theorem name.