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

#![doc = include_str!("readme.md")]
use oak_core::{Language, LanguageCategory};

/// Lean language definition.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct LeanLanguage {}

impl Language for LeanLanguage {
    const NAME: &'static str = "lean";
    const CATEGORY: LanguageCategory = LanguageCategory::Programming;

    type TokenType = crate::lexer::token_type::LeanTokenType;
    type ElementType = crate::parser::element_type::LeanElementType;
    type TypedRoot = crate::ast::LeanRoot;
}

impl LeanLanguage {
    /// Creates a new Lean language instance.
    pub fn new() -> Self {
        Self {}
    }
}

impl Default for LeanLanguage {
    fn default() -> Self {
        Self {}
    }
}