lean_diagnostic_messages
Retrieve compiler diagnostics (errors, warnings, infos) for Lean theorem prover files to identify and resolve code issues.
Instructions
Get compiler diagnostics (errors, warnings, infos) for a Lean file.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file | |
| start_line | No | Filter from line | |
| end_line | No | Filter to line | |
| declaration_name | No | Filter to declaration (slow) |