lean_agentic/
lib.rs

1//! # leanr-core
2//!
3//! Core type theory implementation for Lean 4 in Rust.
4//! This crate provides the trusted kernel with term representation,
5//! universe levels, type checking, and definitional equality.
6
7#![warn(missing_docs)]
8#![deny(unsafe_op_in_unsafe_fn)]
9
10pub mod arena;
11pub mod context;
12pub mod conversion;
13pub mod environment;
14pub mod level;
15pub mod symbol;
16pub mod term;
17pub mod typechecker;
18pub mod unification;
19
20pub use arena::Arena;
21pub use context::Context;
22pub use environment::Environment;
23pub use level::{Level, LevelId};
24pub use symbol::{Symbol, SymbolId, SymbolTable};
25pub use term::{Binder, Term, TermId, TermKind};
26
27/// Result type for core operations
28pub type Result<T> = std::result::Result<T, Error>;
29
30/// Error types for core operations
31#[derive(Debug, Clone)]
32pub enum Error {
33    /// Type checking error
34    TypeError(String),
35
36    /// Universe inconsistency
37    UniverseError(String),
38
39    /// Unification failure
40    UnificationError(String),
41
42    /// Environment lookup failure
43    NotFound(String),
44
45    /// Conversion check failure
46    ConversionError {
47        /// Expected type
48        expected: String,
49        /// Actual type
50        actual: String,
51    },
52
53    /// Internal error (should not happen in production)
54    Internal(String),
55}
56
57impl std::fmt::Display for Error {
58    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
59        match self {
60            Error::TypeError(msg) => write!(f, "Type error: {}", msg),
61            Error::UniverseError(msg) => write!(f, "Universe error: {}", msg),
62            Error::UnificationError(msg) => write!(f, "Unification error: {}", msg),
63            Error::NotFound(msg) => write!(f, "Not found: {}", msg),
64            Error::ConversionError { expected, actual } => {
65                write!(f, "Conversion check failed: {} ≠ {}", expected, actual)
66            }
67            Error::Internal(msg) => write!(f, "Internal error: {}", msg),
68        }
69    }
70}
71
72impl std::error::Error for Error {}
73
74#[cfg(test)]
75mod tests {
76    use super::*;
77
78    #[test]
79    fn test_basic_term_creation() {
80        let arena = Arena::new();
81        let symbols = SymbolTable::new();
82
83        // Test that we can create basic structures
84        assert!(arena.terms() == 0);
85    }
86}
lean_agentic/lib.rs

lean_agentic/
lib.rs
