lean_file_contents
Fetch the complete text of a Lean file, optionally with line numbers, to review source code or verify line references.
Instructions
DEPRECATED: Will be removed soon.
Get the text contents of a Lean file, optionally with line numbers.
Use sparingly (bloats context). Mainly when unsure about line numbers.
Args:
file_path (str): Abs path to Lean file
annotate_lines (bool, optional): Annotate lines with line numbers. Defaults to True.
Returns:
str: File content or error msg
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | ||
| annotate_lines | No |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |