pub fn theorem_proof_exprs_with_defs(
input: &str,
) -> Result<(Vec<ProofExpr>, ProofExpr, Vec<Definition>), ParseError>Expand description
Like theorem_proof_exprs but also returns the document’s ## Define
blocks (Rung 0a) lowered to proof-layer definitions, so the prover can
δ-unfold them. This is the entry the kernel-certified theorem path uses.