pub fn proof_mode_findings(ctx: &CodegenContext) -> Vec<ProofModeIssue>Expand description
Proof-mode diagnostics for Lean transpilation.
Returns human-readable notices for recursive shapes that still fall back to
regular partial Lean defs instead of total proof-mode emission.