lean_run_code
Execute Lean code snippets with required imports to obtain diagnostic feedback and verify theorem correctness.
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 |