Crate oxilean 

OxiLean

A Pure Rust theorem prover and dependent type checker inspired by Lean 4.

This crate is a facade that re-exports all OxiLean library components. Use feature flags to select which components to include.

Features

• kernel (default) - The trusted computing base for type checking
• parse (default) - Concrete syntax to abstract syntax parser
• elab (default) - Surface syntax to kernel terms elaborator
• meta (default) - Metavar-aware WHNF, unification, type class synthesis, and tactics
• codegen - LCNF-based compilation and optimization
• runtime - Runtime system with GC, closures, and bytecode interpretation
• std-lib - Standard library (Nat, Bool, List, etc.)
• lint - Static analysis and lint rules
• build-sys - Build system with incremental compilation
• wasm - WebAssembly support
• full - All components except wasm

Quick Start

// With default features (kernel, parse, elab, meta):
use oxilean::kernel;
use oxilean::parse;

Re-exports

pub use oxilean_kernel as kernel;

pub use oxilean_meta as meta;

pub use oxilean_parse as parse;

pub use oxilean_elab as elab;