lean_run_code
Run a complete, self-contained Lean code snippet to get diagnostics. Use for testing outside open files; include all imports and definitions.
Instructions
Run a complete, self-contained code snippet and return diagnostics.
Has to include all imports and definitions!
Only use for testing outside open files! Keep the user in the loop by editing files instead.
Args:
code (str): Code snippet
Returns:
List[str] | str: Diagnostics msgs or error msg
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| code | Yes |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |