lean_run_code
Read-onlyIdempotent
Execute Lean code snippets with imports to obtain diagnostic feedback for theorem proving verification.
Instructions
Run a code snippet and return diagnostics. Must include all imports.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| code | Yes | Self-contained Lean code with imports |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| success | Yes | Whether code compiled successfully | |
| diagnostics | No | Compiler diagnostics |