Expand description
§leanr-core
Core type theory implementation for Lean 4 in Rust. This crate provides the trusted kernel with term representation, universe levels, type checking, and definitional equality.
Re-exports§
pub use arena::Arena;pub use context::Context;pub use environment::Environment;pub use level::Level;pub use level::LevelId;pub use symbol::Symbol;pub use symbol::SymbolId;pub use symbol::SymbolTable;pub use term::Binder;pub use term::Term;pub use term::TermId;pub use term::TermKind;
Modules§
- arena
- Arena allocator for term hash-consing
- context
- Type context for local variables
- conversion
- Definitional equality and weak head normal form evaluation
- environment
- Global environment for constants and declarations
- level
- Universe levels for Lean’s predicative type theory
- symbol
- Symbol interning for efficient name representation
- term
- Core term representation for dependent type theory
- typechecker
- Trusted type checking kernel
- unification
- Unification and constraint solving for metavariables
Enums§
- Error
- Error types for core operations
Type Aliases§
- Result
- Result type for core operations