Stats
Actions
Tags
From claude-lean4-lsp
Lake language server for Lean provides code intelligence for the Lean proof assistant: diagnostics, go-to-definition, find references, hovers, and symbols for .lean files.
This LSP server requires laketo be installed on your system. Make sure it's available in your PATH before enabling.
Copy this JSON into your .lsp.json to enable this server
Add to your .lsp.json or plugin.json:
{
"lspServers": {
"lean": {
"command": "lake",
"extensionToLanguage": {
".lean": "lean"
},
"args": [
"serve"
]
}
}
}File extensions mapped to language identifiers
Server configuration and transport parameters
lakestdioCommand-line arguments passed to the server process
Initialization options and workspace settings
Initialization Options:
{}Settings:
{}npx claudepluginhub lucianoxu/claude-lean4-lsp