API

class leanclient.client.LeanLSPClient(project_path: str, max_opened_files: int = 4, initial_build: bool = False, prevent_cache_get: bool = False)

Bases: LSPFileManager, BaseLeanLSPClient

LeanLSPClient is a thin wrapper around the Lean language server.

It allows interaction with a subprocess running lake serve via the Language Server Protocol (LSP). This wrapper is blocking, it waits until the language server responds.

Note

Your project_path is the root folder of a Lean project where lakefile.toml is located. This is where lake build and lake serve are run.

All file paths are relative to the project_path.

E.g. “.lake/packages/mathlib/Mathlib/Init.lean” can be a valid path.

To control logging output, configure the ‘leanclient’ logger:

import logging
logging.getLogger('leanclient').setLevel(logging.WARNING)  # Show warnings and errors
logging.getLogger('leanclient').setLevel(logging.DEBUG)    # Show all messages
Parameters:

  • project_path (str) – Path to the root folder of a Lean project.

  • max_opened_files (int) – Maximum number of files to keep open at once. Defaults to 4.

  • initial_build (bool) – Whether to run lake build on initialization. Defaults to False. The Lean LSP server does not require a build to function - it will build dependencies on-demand when files are opened.

  • prevent_cache_get (bool) – Prevent automatic lake exe cache get for mathlib projects. Defaults to False. Useful for tests to avoid repeated cache downloads.

_local_to_uri(local_path: str | PathLike[str]) → str

Convert a local file path to a URI.

User API is based on local file paths (relative to project path) but internally we use URIs. Example:

Parameters:

local_path (str) – Relative file path.

Returns:

URI representation of the file.

Return type:

str

_locals_to_uris(local_paths: list[str]) → list[str]

See _local_to_uri()

static _normalize_local_path(local_path: str | PathLike[str]) → str

Normalize Lean project-local paths to forward slashes.

_open_new_files(paths: list[str], dependency_build_mode: str = 'never') → None

Open new files in the language server.

Parameters:

  • paths (list[str]) – List of relative file paths.

  • dependency_build_mode (str) – Whether to automatically rebuild dependencies. Defaults to “never”.

_read_stdout_loop(stop_event: Event)

Read the stdout of the language server in a separate thread.

This is necessary to avoid blocking the main thread. Dispatches responses to futures and notifications to handlers.

_register_notification_handler(method: str, handler)

Register a handler for a specific notification method.

Parameters:

  • method (str) – Notification method name (e.g., “textDocument/publishDiagnostics”).

  • handler – Callable that takes the notification message as argument.

_rpc_call(uri: str, method: str, params: dict, line: int = 0, character: int = 0, timeout: float = 15) → dict

Make an RPC call to the Lean server.

RPC calls are used for interactive features like widgets. Common methods include: - “Lean.Widget.getWidgets”: Get panel widgets at a position - “Lean.Widget.getInteractiveDiagnostics”: Get diagnostics with embedded widgets

Note

This is an internal method. Use the public widget methods instead.

Parameters:

  • uri (str) – File URI.

  • method (str) – RPC method name (e.g., “Lean.Widget.getWidgets”).

  • params (dict) – Parameters to pass to the RPC method.

  • line (int) – Line number for snapshot lookup (0-indexed). Defaults to 0.

  • character (int) – Character number for snapshot lookup (0-indexed). Defaults to 0.

  • timeout (float) – Timeout in seconds. Defaults to 15.

Returns:

Response from the RPC call.

Return type:

dict

_rpc_connect(uri: str, timeout: float = 10) → str

Connect to Lean RPC for a file and get a session ID.

The Lean server provides RPC capabilities for interactive features like widgets. This method establishes an RPC session for a file, which is required before making RPC calls.

Note

This is an internal method. Session management is handled automatically by the widget methods.

Parameters:

  • uri (str) – File URI (use _local_to_uri to convert local paths).

  • timeout (float) – Timeout in seconds. Defaults to 10.

Returns:

Session ID for use in subsequent RPC calls.

Return type:

str

Raises:

RuntimeError – If session ID cannot be obtained.

_rpc_release_session(uri: str) → None

Release an RPC session for a file.

Called when a file is closed/reopened to prevent stale sessions.

Parameters:

uri (str) – File URI.

_run_event_loop()

Run the asyncio event loop in a separate thread.

_send_notification(method: str, params: dict)

Send a notification to the language server.

Parameters:

  • method (str) – Method name.

  • params (dict) – Parameters for the method.

_send_request(path: str, method: str, params: dict, timeout: float = 30.0) → dict

Send request about a document and return a response or and error.

Parameters:

  • path (str) – Relative file path.

  • method (str) – Method name.

  • params (dict) – Parameters for the method.

  • timeout (float) – Timeout in seconds. Defaults to 30.

Returns:

Response or error.

Return type:

dict

_send_request_async(method: str, params: dict) → Future

Send a request and return an asyncio.Future immediately (non-blocking).

Parameters:

  • method (str) – Method name.

  • params (dict) – Parameters for the method.

Returns:

Future that will be resolved when the response arrives.

Return type:

asyncio.Future

_send_request_retry(path: str, method: str, params: dict, max_retries: int = 1, retry_delay: float = 0.0) → dict

Send requests until no new results are found after a number of retries.

Parameters:

  • path (str) – Relative file path.

  • method (str) – Method name.

  • params (dict) – Parameters for the method.

  • max_retries (int) – Number of times to retry if no new results were found. Defaults to 1.

  • retry_delay (float) – Time to wait between retries. Defaults to 0.0.

Returns:

Final response.

Return type:

dict

_send_request_rpc(method: str, params: dict, is_notification: bool) → int | None

Send a JSON RPC request to the language server.

Parameters:

  • method (str) – Method name.

  • params (dict) – Parameters for the method.

  • is_notification (bool) – Whether the request is a notification.

Returns:

Id of the request if it is not a notification.

Return type:

int | None

_send_request_sync(method: str, params: dict, timeout: float | None = 120.0) → dict

Send a request and block until response arrives.

Parameters:

  • method (str) – Method name.

  • params (dict) – Parameters for the method.

  • timeout (float | None) – Timeout in seconds. Defaults to 120.

Returns:

Response from the language server.

Return type:

dict

_setup_global_handlers()

Setup permanent handlers for diagnostics and file progress notifications.

_unregister_notification_handler(method: str)

Unregister a notification handler.

Parameters:

method (str) – Notification method name.

_uri_to_abs(uri: str) → Path

See _local_to_uri()

_uri_to_local(uri: str) → str

See _local_to_uri()

_wait_for_diagnostics(uris: list[str], inactivity_timeout: float = 15.0, max_timeout: float = 300.0) → bool

Wait until file is loaded or an rpc error occurs.

This method uses an adaptive timeout that resets whenever diagnostics are received. This allows long-running operations to complete while quickly detecting stuck states.

Parameters:

  • uris (list[str]) – List of URIs to wait for diagnostics on.

  • inactivity_timeout (float) – Time to wait since last activity (diagnostics update). Defaults to 15 seconds.

  • max_timeout (float) – Absolute maximum time to wait regardless of activity. Defaults to 300 seconds.

Returns:

True if diagnostics completed successfully, False if timed out.

Return type:

bool

_wait_for_line_range(uris: list[str], start_line: int, end_line: int, inactivity_timeout: float = 3.0) → bool

Wait for specific line range to complete based on parallel processing ranges.

This method polls the current_processing state to determine when the requested line range is no longer being processed. Unlike _wait_for_diagnostics, this doesn’t use LSP’s waitForDiagnostics request since we only care about a subset of the file.

Parameters:

  • uris (list[str]) – List of URIs to wait for.

  • start_line (int) – Start line of range (0-based).

  • end_line (int) – End line of range (0-based, inclusive).

  • inactivity_timeout (float) – Maximum time to wait since last activity.

Returns:

True if completed successfully, False if timed out.

Return type:

bool

apply_code_action_resolve(code_action_resolved: dict) → None

Apply all edits of a resolved code action.

Helper to apply the edits required to resolve a code action. Converts the edits to DocumentContentChange and calls update_file()

First get the code action using get_code_actions(), then resolve it using get_code_action_resolve(). Finally apply the resolved code action using this method.

Note

Does not update the file system, only the in-memory representation of the file in the LSP. Use get_file_content() to get the updated file content.

Parameters:

code_action_resolved (dict) – Resolved code action as returned by get_code_action_resolve().

build_project(get_cache: bool = True)

Build the Lean project by running lake build.

Parameters:

get_cache (bool) – Whether to run lake exe cache get before building.

clear_history()

Clear all stored LSP communication history entries.

Note: History tracking is controlled by the ENABLE_LEANCLIENT_HISTORY environment variable at initialization, or can be enabled at runtime via enable_history = True.

Example

>>> client.enable_history = True
>>> # ... some LSP communications occur ...
>>> len(client.history)
5
>>> client.enable_history = False
>>> client.clear_history()
>>> len(client.history)
0
close(timeout: float | None = 2)

Always close the client when done!

Terminates the language server process and cleans up resources.

Parameters:

timeout (float | None) – Time to wait for the process to terminate. Defaults to 2 seconds.

close_all_files(blocking: bool = True)

Close all open files in the language server.

Parameters:

blocking (bool) – Not blocking can be risky if you close files frequently or reopen them.

close_files(paths: list[str], blocking: bool = True)

Close files in the language server.

Calling this manually is optional, files are automatically closed when max_opened_files is reached.

Parameters:

  • paths (list[str]) – List of relative file paths to close.

  • blocking (bool) – Not blocking can be risky if you close files frequently or reopen them.

create_file_client(file_path: str) → SingleFileClient

Create a SingleFileClient for a file.

Parameters:

file_path (str) – Relative file path.

Returns:

A client for interacting with a single file.

Return type:

SingleFileClient

get_call_hierarchy_incoming(item: dict) → list

Get call hierarchy items that call a symbol.

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

The callHierarchy/incomingCalls method in LSP retrieves incoming call hierarchy items for a specified item. Use get_call_hierarchy_items() first to get an item.

More Information:

Example response:

[
    {
        'from': {
            'data': {'module': 'Mathlib.Data.Finset.Card', 'name': 'Finset.exists_eq_insert_iff'},
            'kind': 14,
            'name': 'Finset.exists_eq_insert_iff',
            'range': {'end': {'character': 39, 'line': 630},
                        'start': {'character': 0, 'line': 618}},
            'selectionRange': {'end': {'character': 28, 'line': 618},
                                'start': {'character': 8, 'line': 618}},
            'uri': 'file://...'
        },
        'fromRanges': [{'end': {'character': 36, 'line': 630},
                        'start': {'character': 10, 'line': 630}}]
    },
    # ...
]
Parameters:

item (dict) – The call hierarchy item.

Returns:

Incoming call hierarchy items.

Return type:

list

get_call_hierarchy_items(path: str, line: int, character: int) → list

Get call hierarchy items at a file position.

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

The textDocument/prepareCallHierarchy method in LSP retrieves call hierarchy items at a specified cursor position. Use a call hierarchy item to get the incoming and outgoing calls: get_call_hierarchy_incoming() and get_call_hierarchy_outgoing().

More Information:

Example response:

[
    {
        'data': {'module': 'LeanTestProject.Basic', 'name': 'add_zero_custom'},
        'kind': 14,
        'name': 'add_zero_custom',
        'range': {'end': {'character': 23, 'line': 1},
                    'start': {'character': 8, 'line': 1}},
        'selectionRange': {'end': {'character': 23, 'line': 1},
                            'start': {'character': 8, 'line': 1}},
        'uri': 'file://...'
    }
]
Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number.

  • character (int) – Character number.

Returns:

Call hierarchy items.

Return type:

list

get_call_hierarchy_outgoing(item: dict) → list

Get outgoing call hierarchy items for a given item.

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

The callHierarchy/outgoingCalls method in LSP retrieves outgoing call hierarchy items for a specified item. Use get_call_hierarchy_items() first to get an item.

More Information:

Example response:

[
    {
        'fromRanges': [{'end': {'character': 52, 'line': 184},
                        'start': {'character': 48, 'line': 184}},
                        {'end': {'character': 66, 'line': 184},
                        'start': {'character': 62, 'line': 184}}],
        'to': {'data': {'module': 'Mathlib.Data.Finset.Insert', 'name': 'Finset.cons'},
                'kind': 14,
                'name': 'Finset.cons',
                'range': {'end': {'character': 8, 'line': 234},
                        'start': {'character': 4, 'line': 234}},
                'selectionRange': {'end': {'character': 8, 'line': 234},
                                'start': {'character': 4, 'line': 234}},
                'uri': 'file://...'}
    }
]
Parameters:

item (dict) – The call hierarchy item.

Returns:

Outgoing call hierarchy items.

Return type:

list

get_code_action_resolve(code_action: dict) → dict

Resolve a code action.

Calls the codeAction/resolve method.

Use get_code_actions() to get the code actions in a file first. Select one and get the resolved code action. Then apply the resolved code action using apply_code_action_resolve().

More information:

Example response:

{
    'title': 'Update #guard_msgs with tactic output',
    'kind': 'quickfix',
    'isPreferred': True,
    'edit': {
        'documentChanges': [
            {
                'textDocument': {
                    'version': 0,
                    'uri': 'file:///home/ooo/Code/leanclient/.test_env/LeanTestProject/Basic.lean'
                },
                'edits': [
                    {
                        'range': {
                            'start': {'line': 12, 'character': 0},
                            'end': {'line': 12, 'character': 15}
                        },
                        'newText': '/-- info: 1 -/\n'
                    }
                ]
            }
        ]
    }
}
Parameters:

code_action (dict) – Code action as returned by get_code_actions() (only one).

Returns:

Resolved code action.

Return type:

dict

get_code_actions(path: str, start_line: int, start_character: int, end_line: int, end_character: int, max_retries: int = 3, retry_delay: float = 0.001) → list

Get code actions for a text range.

The textDocument/codeAction method in LSP returns a list of commands that can be executed to fix or improve the code.

You can resolve the returned code actions using get_code_action_resolve(). Finally you can apply the resolved code action using apply_code_action_resolve().

More information:

Example response:

[
    {
        'title': 'Update #guard_msgs with tactic output',
        'kind': 'quickfix',
        'isPreferred': True,
        'data': {
            'providerResultIndex': 0,
            'providerName': 'Lean.CodeAction.cmdCodeActionProvider',
            'params': {
                'textDocument': {
                    'uri': 'file:///home/ooo/Code/leanclient/.test_env/LeanTestProject/Basic.lean'
                },
                'range': {
                    'start': {'line': 12, 'character': 8},
                    'end': {'line': 12, 'character': 18}
                },
                'context': {
                    'triggerKind': 1,
                    'diagnostics': [
                        {
                            'source': 'Lean 4',
                            'severity': 3,
                            'range': {
                                'start': {'line': 12, 'character': 37},
                                'end': {'line': 12, 'character': 42}
                            },
                            'message': '1',
                            'fullRange': {
                                'start': {'line': 12, 'character': 37},
                                'end': {'line': 12, 'character': 42}
                            }
                        },
                        {
                            'source': 'Lean 4',
                            'severity': 1,
                            'range': {
                                'start': {'line': 12, 'character': 15},
                                'end': {'line': 12, 'character': 26}
                            },
                            'message': '❌️ Docstring on `#guard_msgs` does not match generated message:\n\ninfo: 1',
                            'fullRange': {
                                'start': {'line': 12, 'character': 15},
                                'end': {'line': 12, 'character': 26}
                            }
                        }
                    ]
                }
            }
        }
    }
]
Parameters:

  • path (str) – Relative file path.

  • start_line (int) – Start line.

  • start_character (int) – Start character.

  • end_line (int) – End line.

  • end_character (int) – End character.

  • max_retries (int) – Number of times to retry if no new results were found. Defaults to 3.

  • retry_delay (float) – Time to wait between retries. Defaults to 0.001.

Returns:

Code actions.

Return type:

list

get_completion_item_resolve(item: dict) → str

Resolve a completion item.

The completionItem/resolve method in LSP is used to resolve additional information for a completion item.

More information:

Example response:

# Input item
{"label": "add_lt_of_lt_sub'", ...}

# Detail is:
"b < c - a → a + b < c"
Parameters:

item (dict) – Completion item.

Returns:

Additional detail about the completion item.

Return type:

str

get_completions(path: str, line: int, character: int) → list

Get completion items at a file position.

The textDocument/completion method in LSP provides context-aware code completion suggestions at a specified cursor position. It returns a list of possible completions for partially typed code, suggesting continuations.

Note

The _uri field is added by leanclient to enable later resolution. It is not part of the LSP response.

More information:

Example response:

[
    {'_uri': 'LeanTestProject/Basic.lean',
    'data': ['LeanTestProject.Basic', 9, 15, 0, 'cNat.dvd_add_left'],
    'kind': 23,
    'label': 'dvd_add_left'},
    # ...
]
Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number.

  • character (int) – Character number.

Returns:

Completion items.

Return type:

list

get_declarations(path: str, line: int, character: int) → list

Get locations of declarations at a file position.

The textDocument/declaration method in LSP retrieves the declaration location of a symbol at a specified cursor position.

More information:

Example response:

 [{
    'originSelectionRange': {
        'end': {'character': 7, 'line': 6},
        'start': {'character': 4, 'line': 6}
    },
    'targetRange': {
        'end': {'character': 21, 'line': 370},
        'start': {'character': 0, 'line': 365}
    },
    'targetSelectionRange': {
        'end': {'character': 6, 'line': 370},
        'start': {'character': 0, 'line': 370}
    },
    'targetUri': 'file://...'
}]
Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number.

  • character (int) – Character number.

Returns:

Locations.

Return type:

list

get_definitions(path: str, line: int, character: int) → list

Get location of symbol definition at a file position.

The textDocument/definition method in LSP retrieves the definition location of a symbol at a specified cursor position. Find implementations or definitions of variables, functions, or types within the codebase.

More information:

Example response:

 [{
    'originSelectionRange': {
        'end': {'character': 7, 'line': 6},
        'start': {'character': 4, 'line': 6}
    },
    'targetRange': {
        'end': {'character': 21, 'line': 370},
        'start': {'character': 0, 'line': 365}
    },
    'targetSelectionRange': {
        'end': {'character': 6, 'line': 370},
        'start': {'character': 0, 'line': 370}
    },
    'targetUri': 'file://...'
}]
Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number.

  • character (int) – Character number.

Returns:

Locations.

Return type:

list

get_diagnostics(path: str, start_line: int | None = None, end_line: int | None = None, inactivity_timeout: float = 15.0, max_timeout: float = 300.0) → DiagnosticsResult

Get diagnostics for a file, optionally filtered to a line range.

Supports open-ended ranges (start_line only, end_line only, both, or neither). Opens file if needed and waits for diagnostics to be ready.

Returns a DiagnosticsResult with: - success: True if build succeeded (no errors in ANY diagnostics, not just filtered range).

False if there are errors, fatal errors, or if the wait timed out.

  • diagnostics: List of diagnostic dicts (filtered to range if specified)

The result behaves like a list for backward compatibility - you can iterate, index, and check length directly on the result.

Example usage:

result = client.get_diagnostics("Foo.lean", start_line=10, end_line=20)

# New structured access:
if result.success:
    print("Build succeeded!")
for diag in result.diagnostics:
    print(diag['message'])

# Backward-compatible list access:
for diag in result:  # iterates over diagnostics
    print(diag['message'])
print(len(result))  # number of diagnostics
Parameters:

  • path (str) – Relative file path.

  • start_line (int | None) – Start line (0-based). If None, starts from beginning.

  • end_line (int | None) – End line (0-based, inclusive). If None, goes to end of file.

  • inactivity_timeout (float) – Maximum time to wait since last activity. Defaults to 15 seconds.

Returns:

Structured result with success status and diagnostics list.

Return type:

DiagnosticsResult

Raises:

ValueError – If start_line > end_line

get_document_highlights(path: str, line: int, character: int) → list

Get highlight ranges for a symbol at a file position.

The textDocument/documentHighlight method in LSP returns the highlighted range at a specified cursor position.

More information:

Example response:

[{
    'range': {
        'start': {'line': 5, 'character': 10},
        'end': {'line': 5, 'character': 15}
    },
    'kind': 1
}]
Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number.

  • character (int) – Character number.

Returns:

Document highlights.

Return type:

list

get_document_symbols(path: str) → list

Get all document symbols in a document.

The textDocument/documentSymbol method in LSP retrieves all symbols within a document, providing their names, kinds, and locations.

More information:

Example response:

[
    {
        'kind': 'method',
        'name': 'add_zero_custom',
        'range': {
            'end': {'character': 25, 'line': 9},
            'start': {'character': 0, 'line': 1}
        },
        'selectionRange': {
            'end': {'character': 23, 'line': 1},
            'start': {'character': 8, 'line': 1}}
    },
    # ...
]
Parameters:

path (str) – Relative file path.

Returns:

Document symbols.

Return type:

list

get_env(return_dict: bool = True) → dict | str

Get the environment variables of the project.

Parameters:

return_dict (bool) – Return as dict or string.

Returns:

Environment variables.

Return type:

dict | str

get_file_content(path: str) → str

Get the content of a file as seen by the language server.

Parameters:

path (str) – Relative file path.

Returns:

Content of the file.

Return type:

str

get_folding_ranges(path: str) → list

Get folding ranges in a document.

The textDocument/foldingRange method in LSP returns folding ranges in a document.

More information:

Example response:

[
    {
        'startLine': 0,
        'endLine': 1,
        'kind': 'region'
    },
    # ...
]
Parameters:

path (str) – Relative file path.

Returns:

Folding ranges.

Return type:

list

get_goal(path: str, line: int, character: int) → dict | None

Get proof goal at a file position.

$/lean/plainGoal is a custom lsp request that returns the proof goal at a specified cursor position.

In the VSCode Lean Infoview, this is shown as Tactic state.

Use get_term_goal() to get term goal.

More information:

Note

  • Returns {'goals': [], 'rendered': 'no goals'} if there are no goals left 🎉.

  • Returns None if there are no goals at the position.

Example response:

{
    "goals": [
        "case succ\nn' : Nat\nih : n' + 0 = n'\n⊢ (n' + 0).succ + 0 = (n' + 0).succ"
    ],
    "rendered": "```lean\ncase succ\nn' : Nat\nih : n' + 0 = n'\n⊢ (n' + 0).succ + 0 = (n' + 0).succ\n```"
}
Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number.

  • character (int) – Character number.

Returns:

Proof goals at the position.

Return type:

dict | None

get_hover(path: str, line: int, character: int) → dict | None

Get hover information at a cursor position.

The textDocument/hover method in LSP retrieves hover information, providing details such as type information, documentation, or other relevant data about the symbol under the cursor.

More information:

Example response:

{
    "range": {
        "start": {"line": 4, "character": 2},
        "end": {"line": 4, "character": 8}
    },
    "contents": {
        "value": "The left hand side of an induction arm, `| foo a b c` or `| @foo a b c`\nwhere `foo` is a constructor of the inductive type and `a b c` are the arguments\nto the constructor.\n",
        "kind": "markdown"
    }
}
Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number.

  • character (int) – Character number.

Returns:

Hover information or None if no hover information is available.

Return type:

dict

get_info_trees(path: str, parse: bool = False) → list

Get info trees for a all “method” symbols (e.g. theorems) in a file.

Inserts #info_trees in for each method symbol and analyzes resulting diagnostic messages.

Note

This method currently only returns info trees for symbols of kind “method” (e.g. “theorem”). Further, this method ignores invalid symbols, e.g. if a theorem contains a syntax error.

More information:

Check leanclient.info_tree.parse_info_tree() for more information on the parsed info tree format.

Example response:

[
    '''• command @ ⟨18, 0⟩-⟨18, 52⟩ @ Lean.Elab.Command.elabDeclaration
   • Nat : Type @ ⟨18, 24⟩-⟨18, 27⟩ @ Lean.Elab.Term.elabIdent
     • [.] Nat : some Sort.{?_uniq.127} @ ⟨18, 24⟩-⟨18, 27⟩
     • Nat : Type @ ⟨18, 24⟩-⟨18, 27⟩
   • n (isBinder := true) : Nat @ ⟨18, 20⟩-⟨18, 21⟩
   • n + 0 = n : Prop @ ⟨18, 31⟩-⟨18, 40⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
     • Macro expansion
       n + 0 = n
       ===>
       binrel% Eq✝ (n + 0) n
       • n + 0 = n : Prop @ ⟨18, 31⟩†-⟨18, 40⟩† @ Lean.Elab.Term.Op.elabBinRel
         • n + 0 = n : Prop @ ⟨18, 31⟩†-⟨18, 40⟩†
           • n + 0 : Nat @ ⟨18, 31⟩-⟨18, 36⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
             • Macro expansion
               n + 0
               ===>
               binop% HAdd.hAdd✝ n 0
               • n + 0 : Nat @ ⟨18, 31⟩†-⟨18, 36⟩†
                 • [.] Eq✝ : none @ ⟨18, 31⟩†-⟨18, 40⟩†
                 • [.] HAdd.hAdd✝ : none @ ⟨18, 31⟩†-⟨18, 36⟩†
                 • n : Nat @ ⟨18, 31⟩-⟨18, 32⟩ @ Lean.Elab.Term.elabIdent
                   • [.] n : none @ ⟨18, 31⟩-⟨18, 32⟩
                   • n : Nat @ ⟨18, 31⟩-⟨18, 32⟩
                 • 0 : Nat @ ⟨18, 35⟩-⟨18, 36⟩ @ Lean.Elab.Term.elabNumLit
           • n : Nat @ ⟨18, 39⟩-⟨18, 40⟩ @ Lean.Elab.Term.elabIdent
             • [.] n : none @ ⟨18, 39⟩-⟨18, 40⟩
             • n : Nat @ ⟨18, 39⟩-⟨18, 40⟩
   • CustomInfo(Lean.Elab.Term.AsyncBodyInfo)
     • incomplete (isBinder := true) : ∀ (n : Nat), n + 0 = n @ ⟨18, 8⟩-⟨18, 18⟩
     • n (isBinder := true) : Nat @ ⟨18, 20⟩-⟨18, 21⟩
     • CustomInfo(Lean.Elab.Term.BodyInfo)
       • Tactic @ ⟨18, 44⟩-⟨18, 52⟩
         (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.tacticSorry "sorry")])))
         before
         n : Nat
         ⊢ n + 0 = n
         after no goals
         • Tactic @ ⟨18, 44⟩-⟨18, 46⟩
           "by"
           before
           n : Nat
           ⊢ n + 0 = n
           after no goals
           • Tactic @ ⟨18, 47⟩-⟨18, 52⟩ @ Lean.Elab.Tactic.evalTacticSeq
             (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.tacticSorry "sorry")]))
             before
             n : Nat
             ⊢ n + 0 = n
             after no goals
             • Tactic @ ⟨18, 47⟩-⟨18, 52⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
               (Tactic.tacticSeq1Indented [(Tactic.tacticSorry "sorry")])
               before
               n : Nat
               ⊢ n + 0 = n
               after no goals
               • Tactic @ ⟨18, 47⟩-⟨18, 52⟩ @ Lean.Parser.Tactic._aux_Init_Tactics___macroRules_Lean_Parser_Tactic_tacticSorry_1
                 (Tactic.tacticSorry "sorry")
                 before
                 n : Nat
                 ⊢ n + 0 = n
                 after no goals
                 • Tactic @ ⟨18, 47⟩†-⟨18, 52⟩† @ Lean.Elab.Tactic.evalExact
                   (Tactic.exact "exact" (Term.sorry "sorry"))
                   before
                   n : Nat
                   ⊢ n + 0 = n
                   after no goals
                   • sorry : n + 0 = n @ ⟨18, 47⟩†-⟨18, 52⟩† @ Lean.Elab.Term.elabSorry
     • incomplete (isBinder := true) : ∀ (n : Nat), n + 0 = n @ ⟨18, 8⟩-⟨18, 18⟩'''

     ...
]
Parameters:

  • path (str) – Relative file path.

  • parse (bool) – Whether to parse the info trees. Parsing is experimental! Defaults to False.

Returns:

List of info trees as raw strings or parsed into structured data if parse is True.

Return type:

list

get_interactive_diagnostics(path: str, start_line: int | None = None, end_line: int | None = None, extract_widgets: bool = False) → list[dict]

Get interactive diagnostics with embedded widget data.

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

Interactive diagnostics include widgets embedded in diagnostic messages, such as images from #png or custom error visualizations.

This uses the Lean RPC method Lean.Widget.getInteractiveDiagnostics.

Parameters:

  • path (str) – Relative file path.

  • start_line (int | None) – Start line (0-indexed). If None, gets all diagnostics.

  • end_line (int | None) – End line (0-indexed, exclusive). If None, gets all diagnostics.

  • extract_widgets (bool) – If True, extract and return widget instances from the diagnostics instead of the full diagnostic objects. Defaults to False.

Returns:

List of interactive diagnostic objects, or list of widget

instance dictionaries if extract_widgets is True.

Return type:

list[dict]

get_module_imported_by(module: dict) → list[dict]

Get all modules that import this module (reverse dependencies).

The $/lean/moduleHierarchy/importedBy method returns all modules that import the given module.

More information:

Example response format is the same as get_module_imports().

Note

Returns empty list when import data unavailable. Use prepare_module_hierarchy() first to ensure file is processed.

Parameters:

module (dict) – Module dict from prepare_module_hierarchy().

Returns:

List of imports in same format as get_module_imports().

Return type:

list[dict]

get_module_imports(module: dict) → list[dict]

Get all imports of a module.

The $/lean/moduleHierarchy/imports method returns all modules imported by the given module (its dependencies).

More information:

Example response:

[
    {
        'module': {'name': 'Mathlib', 'uri': 'file://...'},
        'kind': {
            'isPrivate': False,
            'isAll': False,
            'metaKind': 'nonMeta'
        }
    }
]

Note

Returns empty list when import data unavailable. Use prepare_module_hierarchy() first to ensure file is processed.

Parameters:

module (dict) – Module dict from prepare_module_hierarchy().

Returns:

List of imports.

Return type:

list[dict]

get_references(path: str, line: int, character: int, include_declaration: bool = False, max_retries: int = 3, retry_delay: float = 0.001) → list

Get locations of references to a symbol at a file position.

In LSP, the textDocument/references method provides the locations of all references to a symbol at a given cursor position.

More information:

Example response:

[
    {
        'range': {
            'end': {'character': 14, 'line': 7},
            'start': {'character': 12, 'line': 7}
        },
        'uri': 'file://...'
    },
    # ...
]
Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number.

  • character (int) – Character number.

  • include_declaration (bool) – Whether to include the declaration itself in the results. Defaults to False.

  • max_retries (int) – Number of times to retry if no new results were found. Defaults to 3.

  • retry_delay (float) – Time to wait between retries. Defaults to 0.001.

Returns:

Locations.

Return type:

list

get_semantic_tokens(path: str) → list

Get semantic tokens for the entire document.

The textDocument/semanticTokens/full method in LSP returns semantic tokens for the entire document.

Tokens are formated as: [line, char, length, token_type]

See get_semantic_tokens_range() for limiting to parts of a document.

More information:

Example response:

[
    [1, 0, 7, "keyword"],
    [1, 25, 1, "variable"],
    [1, 36, 1, "variable"],
    # ...
]
Parameters:

path (str) – Relative file path.

Returns:

Semantic tokens.

Return type:

list

get_semantic_tokens_range(path: str, start_line: int, start_character: int, end_line: int, end_character: int) → list

Get semantic tokens for a range in a document.

See get_semantic_tokens_full() for more information.

Parameters:

  • path (str) – Relative file path.

  • start_line (int) – Start line.

  • start_character (int) – Start character.

  • end_line (int) – End line.

  • end_character (int) – End character.

Returns:

Semantic tokens.

Return type:

list

get_term_goal(path: str, line: int, character: int) → dict | None

Get term goal at a file position.

$/lean/plainTermGoal is a custom lsp request that returns the term goal at a specified cursor position.

In the VSCode Lean Infoview, this is shown as Expected type.

Use get_goal() for the full proof goal.

More information:

Note

Returns None if there are is no term goal at the position.

Example response:

{
    'range': {
        'start': {'line': 9, 'character': 8},
        'end': {'line': 9, 'character': 20}
    },
    'goal': "n' : Nat\nih : n' + 0 = n'\n⊢ ∀ (n m : Nat), n + m.succ = (n + m).succ"
}
Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number.

  • character (int) – Character number.

Returns:

Term goal at the position.

Return type:

dict | None

get_type_definitions(path: str, line: int, character: int) → list

Get locations of type definition of a symbol at a file position.

The textDocument/typeDefinition method in LSP returns the location of a symbol’s type definition based on the cursor’s position.

More information:

Example response:

 [{
    'originSelectionRange': {
        'end': {'character': 7, 'line': 6},
        'start': {'character': 4, 'line': 6}
    },
    'targetRange': {
        'end': {'character': 21, 'line': 370},
        'start': {'character': 0, 'line': 365}
    },
    'targetSelectionRange': {
        'end': {'character': 6, 'line': 370},
        'start': {'character': 0, 'line': 370}
    },
    'targetUri': 'file://...'
}]
Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number.

  • character (int) – Character number.

Returns:

Locations.

Return type:

list

get_widget_source(path: str, line: int, character: int, widget: dict) → dict

Get the source code/data for rendering a widget.

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

This retrieves the JavaScript module hash and props needed to render a widget instance. The widget parameter should be a widget instance returned from get_widgets or get_interactive_diagnostics.

This uses the Lean RPC method Lean.Widget.getWidgetSource.

Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number (0-indexed).

  • character (int) – Character number (0-indexed).

  • widget (dict) – Widget instance with at least ‘id’ and ‘javascriptHash’ fields.

Returns:

Widget source information including JavaScript module data.

Return type:

dict

get_widgets(path: str, line: int, character: int) → list[dict]

Get panel widgets at a file position.

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

Panel widgets are interactive UI elements displayed in the Lean infoview, such as proof state visualizations, #png images, or custom widgets.

This uses the Lean RPC method Lean.Widget.getWidgets.

Example response:

[
    {
        'id': 'widget-123',
        'javascriptHash': 'abc123...',
        'range': {'start': {'line': 5, 'character': 0}, ...},
        'name?': 'ProofWidgets.HtmlDisplay',
        'props': {'html': {...}}  # Widget-specific data
    }
]
Parameters:

  • path (str) – Relative file path.

  • line (int) – Line number (0-indexed).

  • character (int) – Character number (0-indexed).

Returns:

List of widget instances at the position.

Return type:

list[dict]

open_file(path: str, dependency_build_mode: str = 'never', force_reopen: bool = False) → None

Open a file in the language server.

Use get_diagnostics() to get diagnostics for the file.

Parameters:

  • path (str) – Relative file path to open.

  • dependency_build_mode (str) – Whether to automatically rebuild dependencies. Defaults to “never”. Can be “once”, “never” or “always”.

  • force_reopen (bool) – If True, always close and reopen the file. If False (default), sync file content from disk using update if already open.

open_files(paths: list[str], dependency_build_mode: str = 'never', force_reopen: bool = False) → None

Open files in the language server.

Use get_diagnostics() to get diagnostics.

Note

Opening multiple files is typically faster than opening them sequentially.

Parameters:

  • paths (list[str]) – List of relative file paths to open.

  • dependency_build_mode (str) – Whether to automatically rebuild dependencies. Defaults to “never”. Can be “once”, “never” or “always”.

  • force_reopen (bool) – If True, close and reopen files that are already open. If False (default), sync content from disk using update for already-open files.

prepare_module_hierarchy(path: str) → dict | None

Prepare module hierarchy for a file.

The $/lean/prepareModuleHierarchy method returns module information for a file, including its name and URI. This is the entry point for exploring the module hierarchy - call this first before getting imports.

The file is automatically opened and processed to ensure import data is available.

More information:

Example response:

{
    'name': 'Mathlib.Data.List.Basic',
    'uri': 'file:///path/.lake/packages/mathlib/...',
    'data': None
}
Parameters:

path (str) – Relative file path.

Returns:

Module info or None.

Return type:

dict | None

update_file(path: str, changes: list[DocumentContentChange]) → None

Update a file in the language server.

Note

Changes are not written to disk! Use get_file_content() to get the current content of a file, as seen by the language server.

Use get_diagnostics() to get diagnostics after the update. Raises a FileNotFoundError if the file is not open.

Parameters:
update_file_content(path: str, content: str) → None

Update the entire content of a file in the language server.

This is a convenience method that replaces the entire file content. More efficient than closing and reopening when the file is already open.

Note

Changes are not written to disk! This only updates the LSP server’s view.

Use get_diagnostics() to get diagnostics after the update. Raises a FileNotFoundError if the file is not open.

Parameters:

  • path (str) – Relative file path to update.

  • content (str) – New complete file content.




class leanclient.single_file_client.SingleFileClient(client: LeanLSPClient, file_path: str)

A simplified API for interacting with a single file only.

See leanclient.client.LeanLSPClient for information.

Can also be created from a client using leanclient.client.LeanLSPClient.create_file_client().

Parameters:

  • client (LeanLSPClient) – The LeanLSPClient instance to use.

  • file_path (str) – The path to the file to interact with.

apply_code_action_resolve(code_action_resolved: dict) → None

See leanclient.client.LeanLSPClient.apply_code_action_resolve()

build_project(get_cache: bool = True)

Build the Lean project by running lake build.

Parameters:

get_cache (bool) – Whether to run lake exe cache get before building.

close_file(blocking: bool = True)

Close the file.

Calling this manually is optional, files are automatically closed when max_opened_files is reached.

Parameters:

blocking (bool) – Not blocking can be risky if you close files frequently or reopen them.

get_call_hierarchy_incoming(item: dict) → list

See leanclient.client.LeanLSPClient.get_call_hierarchy_incoming()

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

get_call_hierarchy_items(line: int, character: int) → list

See leanclient.client.LeanLSPClient.get_call_hierarchy_items()

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

get_call_hierarchy_outgoing(item: dict) → list

See leanclient.client.LeanLSPClient.get_call_hierarchy_outgoing()

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

get_code_action_resolve(code_action: dict) → dict

See leanclient.client.LeanLSPClient.get_code_action_resolve()

get_code_actions(start_line: int, start_character: int, end_line: int, end_character: int) → list

See leanclient.client.LeanLSPClient.get_code_actions()

get_completion_item_resolve(item: dict) → str

See leanclient.client.LeanLSPClient.get_completion_item_resolve()

get_completions(line: int, character: int) → list

See leanclient.client.LeanLSPClient.get_completions()

get_declarations(line: int, character: int) → list

See leanclient.client.LeanLSPClient.get_declarations()

get_definitions(line: int, character: int) → list

See leanclient.client.LeanLSPClient.get_definitions()

get_diagnostics(start_line: int | None = None, end_line: int | None = None, inactivity_timeout: float = 3.0)

See leanclient.client.LeanLSPClient.get_diagnostics()

get_document_highlights(line: int, character: int) → list

See leanclient.client.LeanLSPClient.get_document_highlights()

get_document_symbols() → list

See leanclient.client.LeanLSPClient.get_document_symbols()

get_file_content() → str

See leanclient.client.LeanLSPClient.get_file_content()

get_folding_ranges() → list

See leanclient.client.LeanLSPClient.get_folding_ranges()

get_goal(line: int, character: int) → dict

See leanclient.client.LeanLSPClient.get_goal()

get_hover(line: int, character: int) → dict

See leanclient.client.LeanLSPClient.get_hover()

get_info_trees(parse: bool = False) → list

See leanclient.client.LeanLSPClient.get_info_trees()

get_interactive_diagnostics(start_line: int | None = None, end_line: int | None = None, extract_widgets: bool = False) → list[dict]

See leanclient.client.LeanLSPClient.get_interactive_diagnostics()

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

get_module_imported_by(module: dict) → list[dict]

See leanclient.client.LeanLSPClient.get_module_imported_by()

get_module_imports(module: dict) → list[dict]

See leanclient.client.LeanLSPClient.get_module_imports()

get_references(line: int, character: int, include_declaration: bool = False, max_retries: int = 3, retry_delay: float = 0.001) → list

See leanclient.client.LeanLSPClient.get_references()

get_semantic_tokens() → list

See leanclient.client.LeanLSPClient.get_semantic_tokens()

get_semantic_tokens_range(start_line: int, start_character: int, end_line: int, end_character: int) → list

See leanclient.client.LeanLSPClient.get_semantic_tokens_range()

get_term_goal(line: int, character: int) → dict

See leanclient.client.LeanLSPClient.get_term_goal()

get_type_definitions(line: int, character: int) → list

See leanclient.client.LeanLSPClient.get_type_definitions()

get_widget_source(line: int, character: int, widget: dict) → dict

See leanclient.client.LeanLSPClient.get_widget_source()

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

get_widgets(line: int, character: int) → list[dict]

See leanclient.client.LeanLSPClient.get_widgets()

Experimental

This method is experimental. Use with caution. Warnings are logged via the ‘leanclient’ logger.

open_file(dependency_build_mode: str = 'never', force_reopen: bool = False) → None

See leanclient.client.LeanLSPClient.open_file()

prepare_module_hierarchy() → dict | None

See leanclient.client.LeanLSPClient.prepare_module_hierarchy()

update_file(changes: list[DocumentContentChange]) → list

See leanclient.client.LeanLSPClient.update_file()

update_file_content(content: str) → None

See leanclient.client.LeanLSPClient.update_file_content()




class leanclient.pool.LeanClientPool(project_path: str, num_workers: int | None = None, **kwargs)

Parallel processing of Lean files using multiple language servers.

Use this context manager for parallel processing of multiple Lean files. It is based on Python’s multiprocessing.Pool and uses one LeanLSPClient per worker.

Attention

Windows is not supported for LeanClientPool, it might work but requires extra setup.

Tasks are defined as functions with a single argument, a leanclient.file_client.SingleFileClient instance.

def hover_task(client: SingleFileClient):
    return client.get_hover(1, 1)["contents"]["value"]

def fun_len_task(client):
    num_symbols = len(client.get_document_symbol())
    num_tokens = len(client.get_semantic_tokens())
    return num_tokens / num_symbols

Example use:

from leanclient import LeanClientPool

file_paths = ["path/to/file1.lean", "path/to/file2.lean", ...]

with LeanClientPool("path/to/project") as pool:
    results = pool.map(hover_task, file_paths)

    # Or use submit for more control
    futures = [pool.submit(fun_len_task, file) for file in file_paths]
    results2 = [fut.get() for fut in futures]

Note

By default, the initial_build is turned off and prevent_cache_get is enabled in all workers. Use the initial_build / prevent_cache_get kwargs to influence this.

Parameters:

  • project_path (str) – The path to the Lean project.

  • num_workers (int | None) – The number of workers to use. Defaults to 70% of CPU cores.

  • **kwargs – Additional arguments to pass to leanclient.client.LeanLSPClient.

map(task: Callable[[SingleFileClient], None], file_paths: list, batch_size: int = 1, verbose: bool = False) → list

Parallel file processing.

See LeanClientPool for example use.

Note

batch_size > 1 requires initializing the pool with max_opened_files > 1.

Parameters:

  • task (callable) – The task to execute. Must take a SingleFileClient as its only argument.

  • file_paths (list) – A list of file paths to process.

  • batch_size (int) – Batching allows the language server to open multiple files in parallel. Typically faster but requires more resources (mainly memory). Beware of large batch_sizes. Defaults to 1.

  • verbose (bool) – Show a progress bar. Defaults to False.

Returns:

The result of the task for each file.

Return type:

list

submit(task: Callable[[SingleFileClient], None], file_path: str) → Any

Submit an asynchronous task to the pool.

Example use:

with pool:
    futures = [pool.submit(task, file) for file in file_paths]
    results = [fut.get() for fut in futures]
Parameters:

  • task (callable) – The task to execute. Must take a SingleFileClient as its only argument.

  • file_path (str) – The path to the file to process.

Returns:

The result of the task.

Return type:

Any




utils

class leanclient.utils.DocumentContentChange(text: str, start: Tuple[int, int] | None = None, end: Tuple[int, int] | None = None)

Bases: object

Represents a change in a document.

end: Tuple[int, int] | None = None
get_dict() → dict
is_full_change() → bool
start: Tuple[int, int] | None = None
text: str
class leanclient.utils.SemanticTokenProcessor(token_types: list[str])

Bases: object

Converts semantic token response using a token legend.

This function is a reverse translation of the LSP specification: Semantic Tokens Full Request

Token modifiers are ignored for speed gains, since they are not used. See: LanguageFeatures.lean

leanclient.utils.apply_changes_to_text(text: str, changes: list[DocumentContentChange]) → str

Apply LSP-style incremental changes to text.

leanclient.utils.experimental(func)

Decorator to mark a method as experimental.

leanclient.utils.extract_widgets_from_interactive_diag(diag: dict) → list[dict]

Recursively extract widget instances from interactive diagnostic message data.

The interactive diagnostic message structure is: {

“message”: {
“tag”: [
{
“widget”: {

“wi”: { “id”: “…”, “props”: {…}, … }, “alt”: {…}

}

]

}

}

Parameters:

diag – Interactive diagnostic dictionary.

Returns:

List of widget instance dictionaries.

leanclient.utils.get_diagnostics_in_range(diagnostics: list, start_line: int, end_line: int) → list

Find overlapping diagnostics for a range of lines.

Uses fullRange (with fallback to range) for filtering to capture the semantic span of errors, as Lean may truncate range for display purposes.

Parameters:

  • diagnostics (list) – List of diagnostics.

  • start_line (int) – Start line.

  • end_line (int) – End line.

Returns:

Overlapping diagnostics.

Return type:

list

leanclient.utils.needs_mathlib_cache_get(project_path: Path) → bool

Check if lake exe cache get should be run for this project.

Returns True only when mathlib is a dependency AND cache isn’t extracted yet.

Parameters:

project_path – Path to the Lean project root directory.

Returns:

True if cache get should be run, False to skip it.

Return type:

bool

leanclient.utils.normalize_newlines(text: str) → str

Convert CRLF sequences to LF for stable indexing.

info_tree

leanclient.info_tree.parse_info_tree(info_tree_str: str) → dict

Parses a Lean info tree string into a nested Python dictionary structure.

Attention:

This function is experimental and may change in future versions.

Processes the textual representation of a Lean info tree. It currently supports extracting:

  • Indentation-based hierarchy

  • Node text

  • Node type

  • Source code range

  • Elaborator information

  • Additional metadata

  • Goal states for tactic nodes



Note:

Given the complexity of Lean’s info trees, this function only covers a small subset of structures. Further manual parsing might be required.

Example Output:

{'text': '[Command] @ ⟨19, 0⟩-⟨19, 52⟩ @ Lean.Elab.Command.elabDeclaration', 'children': [{'text': '[Term] Nat : Type @ ⟨19, 24⟩-⟨19, 27⟩ @ Lean.Elab.Term.elabIdent', 'children': [{'text': '[Completion-Id] Nat : some Sort.{?_uniq.131} @ ⟨19, 24⟩-⟨19, 27⟩', 'children': [{'text': '[Term] Nat : Type @ ⟨19, 24⟩-⟨19, 27⟩', 'children': [], 'type': 'Term', 'range': {'start': {'line': 19, 'character': 24, 'synthetic': False}, 'end': {'line': 19, 'character': 27, 'synthetic': False}}}], 'type': 'Completion-Id', 'range': {'start': {'line': 19, 'character': 24, 'synthetic': False}, 'end': {'line': 19, 'character': 27, 'synthetic': False}}}, {'text': '[Term] n (isBinder := true) : Nat @ ⟨19, 20⟩-⟨19, 21⟩', 'children': [], 'type': 'Term', 'range': {'start': {'line': 19, 'character': 20, 'synthetic': False}, 'end': {'line': 19, 'character': 21, 'synthetic': False}}}, {'text': '[Term] n + 0 = n : Prop @ ⟨19, 31⟩-⟨19, 40⟩ @ «_aux_Init_Notation___macroRules_term_=__2»', 'children': [{'text': '[MacroExpansion]', 'children': [{'text': '[Term] n + 0 = n : Prop @ ⟨19, 31⟩†-⟨19, 40⟩† @ Lean.Elab.Term.Op.elabBinRel', 'children': [{'text': '[Term] n + 0 = n : Prop @ ⟨19, 31⟩†-⟨19, 40⟩†', 'children': [{'text': '[Term] n + 0 : Nat @ ⟨19, 31⟩-⟨19, 36⟩ @ «_aux_Init_Notation___macroRules_term_+__2»', 'children': [{'text': '[MacroExpansion]', 'children': [{'text': '[Term] n + 0 : Nat @ ⟨19, 31⟩†-⟨19, 36⟩†', 'children': [{'text': '[Completion-Id] Eq✝ : none @ ⟨19, 31⟩†-⟨19, 40⟩†', 'children': [{'text': '[Completion-Id] HAdd.hAdd✝ : none @ ⟨19, 31⟩†-⟨19, 36⟩†', 'children': [{'text': '[Term] n : Nat @ ⟨19, 31⟩-⟨19, 32⟩ @ Lean.Elab.Term.elabIdent', 'children': [{'text': '[Completion-Id] n : none @ ⟨19, 31⟩-⟨19, 32⟩', 'children': [{'text': '[Term] n : Nat @ ⟨19, 31⟩-⟨19, 32⟩', 'children': [{'text': '[Term] 0 : Nat @ ⟨19, 35⟩-⟨19, 36⟩ @ Lean.Elab.Term.elabNumLit', 'children': [], 'type': 'Term', 'range': {'start': {'line': 19, 'character': 35, 'synthetic': False}, 'end': {'line': 19, 'character': 36, 'synthetic': False}}, 'elaborator': 'Lean.Elab.Term.elabNumLit'}], 'type': 'Term', 'range': {'start': {'line': 19, 'character': 31, 'synthetic': False}, 'end': {'line': 19, 'character': 32, 'synthetic': False}}}], 'type': 'Completion-Id', 'range': {'start': {'line': 19, 'character': 31, 'synthetic': False}, 'end': {'line': 19, 'character': 32, 'synthetic': False}}}], 'type': 'Term', 'range': {'start': {'line': 19, 'character': 31, 'synthetic': False}, 'end': {'line': 19, 'character': 32, 'synthetic': False}}, 'elaborator': 'Lean.Elab.Term.elabIdent'}], 'type': 'Completion-Id', 'range': {'start': {'line': 19, 'character': 31, 'synthetic': True}, 'end': {'line': 19, 'character': 36, 'synthetic': True}}}, {'text': '[Term] n : Nat @ ⟨19, 39⟩-⟨19, 40⟩ @ Lean.Elab.Term.elabIdent', 'children': [{'text': '[Completion-Id] n : none @ ⟨19, 39⟩-⟨19, 40⟩', 'children': [{'text': '[Term] n : Nat @ ⟨19, 39⟩-⟨19, 40⟩', 'children': [], 'type': 'Term', 'range': {'start': {'line': 19, 'character': 39, 'synthetic': False}, 'end': {'line': 19, 'character': 40, 'synthetic': False}}}], 'type': 'Completion-Id', 'range': {'start': {'line': 19, 'character': 39, 'synthetic': False}, 'end': {'line': 19, 'character': 40, 'synthetic': False}}}], 'type': 'Term', 'range': {'start': {'line': 19, 'character': 39, 'synthetic': False}, 'end': {'line': 19, 'character': 40, 'synthetic': False}}, 'elaborator': 'Lean.Elab.Term.elabIdent'}], 'type': 'Completion-Id', 'range': {'start': {'line': 19, 'character': 31, 'synthetic': True}, 'end': {'line': 19, 'character': 40, 'synthetic': True}}}], 'type': 'Term', 'range': {'start': {'line': 19, 'character': 31, 'synthetic': True}, 'end': {'line': 19, 'character': 36, 'synthetic': True}}}], 'type': 'MacroExpansion', 'extra': 'n + 0

===> binop% HAdd.hAdd✝ n 0’}], ‘type’: ‘Term’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 31, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 36, ‘synthetic’: False}}}], ‘type’: ‘Term’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 31, ‘synthetic’: True}, ‘end’: {‘line’: 19, ‘character’: 40, ‘synthetic’: True}}}], ‘type’: ‘Term’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 31, ‘synthetic’: True}, ‘end’: {‘line’: 19, ‘character’: 40, ‘synthetic’: True}}, ‘elaborator’: ‘Lean.Elab.Term.Op.elabBinRel’}], ‘type’: ‘MacroExpansion’, ‘extra’: ‘n + 0 = n ===> binrel% Eq✝ (n + 0) n’}], ‘type’: ‘Term’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 31, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 40, ‘synthetic’: False}}}, {‘text’: ‘[CustomInfo(Lean.Elab.Term.AsyncBodyInfo)]’, ‘children’: [{‘text’: ‘[Term] incomplete (isBinder := true) : ∀ (n : Nat), n + 0 = n @ ⟨19, 8⟩-⟨19, 18⟩’, ‘children’: [{‘text’: ‘[Term] n (isBinder := true) : Nat @ ⟨19, 20⟩-⟨19, 21⟩’, ‘children’: [], ‘type’: ‘Term’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 20, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 21, ‘synthetic’: False}}}, {‘text’: ‘[CustomInfo(Lean.Elab.Term.BodyInfo)]’, ‘children’: [{‘text’: ‘[Tactic] @ ⟨19, 44⟩-⟨19, 52⟩’, ‘children’: [{‘text’: ‘[Tactic] @ ⟨19, 44⟩-⟨19, 46⟩’, ‘children’: [{‘text’: ‘[Tactic] @ ⟨19, 47⟩-⟨19, 52⟩ @ Lean.Elab.Tactic.evalTacticSeq’, ‘children’: [{‘text’: ‘[Tactic] @ ⟨19, 47⟩-⟨19, 52⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented’, ‘children’: [{‘text’: ‘[Tactic] @ ⟨19, 47⟩-⟨19, 52⟩ @ Lean.Parser.Tactic._aux_Init_Tactics___macroRules_Lean_Parser_Tactic_tacticSorry_1’, ‘children’: [{‘text’: ‘[Tactic] @ ⟨19, 47⟩†-⟨19, 52⟩† @ Lean.Elab.Tactic.evalExact’, ‘children’: [{‘text’: ‘[Term] sorry : n + 0 = n @ ⟨19, 47⟩†-⟨19, 52⟩† @ Lean.Elab.Term.elabSorry’, ‘children’: [], ‘type’: ‘Term’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 47, ‘synthetic’: True}, ‘end’: {‘line’: 19, ‘character’: 52, ‘synthetic’: True}}, ‘elaborator’: ‘Lean.Elab.Term.elabSorry’}], ‘type’: ‘Tactic’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 47, ‘synthetic’: True}, ‘end’: {‘line’: 19, ‘character’: 52, ‘synthetic’: True}}, ‘elaborator’: ‘Lean.Elab.Tactic.evalExact’, ‘extra’: ‘(Tactic.exact “exact” (Term.sorry “sorry”)) before n : Nat ⊢ n + 0 = n after no goals’}], ‘type’: ‘Tactic’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 47, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 52, ‘synthetic’: False}}, ‘elaborator’: ‘Lean.Parser.Tactic._aux_Init_Tactics___macroRules_Lean_Parser_Tactic_tacticSorry_1’, ‘extra’: ‘(Tactic.tacticSorry “sorry”) before n : Nat ⊢ n + 0 = n after no goals’}], ‘type’: ‘Tactic’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 47, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 52, ‘synthetic’: False}}, ‘elaborator’: ‘Lean.Elab.Tactic.evalTacticSeq1Indented’, ‘extra’: ‘(Tactic.tacticSeq1Indented [(Tactic.tacticSorry “sorry”)]) before n : Nat ⊢ n + 0 = n after no goals’}], ‘type’: ‘Tactic’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 47, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 52, ‘synthetic’: False}}, ‘elaborator’: ‘Lean.Elab.Tactic.evalTacticSeq’, ‘extra’: ‘(Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.tacticSorry “sorry”)])) before n : Nat ⊢ n + 0 = n after no goals’}], ‘type’: ‘Tactic’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 44, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 46, ‘synthetic’: False}}, ‘extra’: ‘“by” before n : Nat ⊢ n + 0 = n after no goals’}], ‘type’: ‘Tactic’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 44, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 52, ‘synthetic’: False}}, ‘extra’: ‘(Term.byTactic “by” (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.tacticSorry “sorry”)]))) before n : Nat ⊢ n + 0 = n after no goals’}], ‘type’: ‘CustomInfo(Lean.Elab.Term.BodyInfo)’}, {‘text’: ‘[Term] incomplete (isBinder := true) : ∀ (n : Nat), n + 0 = n @ ⟨19, 8⟩-⟨19, 18⟩’, ‘children’: [], ‘type’: ‘Term’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 8, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 18, ‘synthetic’: False}}}], ‘type’: ‘Term’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 8, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 18, ‘synthetic’: False}}}], ‘type’: ‘CustomInfo(Lean.Elab.Term.AsyncBodyInfo)’}], ‘type’: ‘Term’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 24, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 27, ‘synthetic’: False}}, ‘elaborator’: ‘Lean.Elab.Term.elabIdent’}], ‘type’: ‘Command’, ‘range’: {‘start’: {‘line’: 19, ‘character’: 0, ‘synthetic’: False}, ‘end’: {‘line’: 19, ‘character’: 52, ‘synthetic’: False}}, ‘elaborator’: ‘Lean.Elab.Command.elabDeclaration’}

​

Args:

info_tree_str (str): The string representation of a Lean info tree.

Returns:

dict: A nested dictionary representing the parsed info tree.