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
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

#![doc = include_str!("readme.md")]
#[cfg(feature = "oak-highlight")]
pub mod highlighter;

use crate::language::LeanLanguage;
#[cfg(feature = "lsp")]
use oak_lsp::{LanguageService, MemoryVfs, WorkspaceManager};
#[cfg(feature = "lsp")]
pub struct LeanLanguageService {
    config: LeanLanguage,
    vfs: MemoryVfs,
    workspace: WorkspaceManager,
}
#[cfg(feature = "lsp")]
impl LeanLanguageService {
    pub fn new(config: LeanLanguage) -> Self {
        Self { config, vfs: MemoryVfs::default(), workspace: WorkspaceManager::default() }
    }
}
#[cfg(feature = "lsp")]
impl LanguageService for LeanLanguageService {
    type Lang = LeanLanguage;
    type Vfs = MemoryVfs;
    fn vfs(&self) -> &Self::Vfs {
        &self.vfs
    }
    fn workspace(&self) -> &WorkspaceManager {
        &self.workspace
    }
}