Expand description
Parsing Lean/Lake diagnostic output.
This starts intentionally conservative. The parser should preserve raw messages and only structure fields it can infer reliably.
Functionsยง
- parse_
lean_ diagnostics - Parse Lean diagnostics from stderr/stdout text.