oak-lean 0.0.11

Lean theorem prover language parser with support for dependent types and formal verification.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13

#![doc = include_str!("readme.md")]
use crate::lsp::LeanLanguageService;
use oak_vfs::MemoryVfs;

/// Start an MCP server for Lean semantics (Stdio).
pub async fn serve_lean_mcp(_vfs: MemoryVfs) {
    let service = LeanLanguageService::new(crate::language::LeanLanguage::default());
    let server = oak_mcp::McpServer::new(service);

    let reader = tokio::io::BufReader::new(tokio::io::stdin());
    let writer = tokio::io::BufWriter::new(tokio::io::stdout());
    server.run(reader, writer).await.unwrap()
}