oxilean 0.1.2

OxiLean - A Pure Rust theorem prover and dependent type checker inspired by Lean 4
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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71

//! # 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
//!
//! ```rust
//! // With default features (kernel, parse, elab, meta):
//! use oxilean::kernel;
//! use oxilean::parse;
//! ```

#![deny(unsafe_code)]
#![warn(missing_docs)]

/// The trusted computing base for type checking.
#[cfg(feature = "kernel")]
pub use oxilean_kernel as kernel;

/// Metavar-aware WHNF, unification, type class synthesis, and tactics.
#[cfg(feature = "meta")]
pub use oxilean_meta as meta;

/// Concrete syntax to abstract syntax parser.
#[cfg(feature = "parse")]
pub use oxilean_parse as parse;

/// Surface syntax to kernel terms elaborator.
#[cfg(feature = "elab")]
pub use oxilean_elab as elab;

/// LCNF-based compilation and optimization.
#[cfg(feature = "codegen")]
pub use oxilean_codegen as codegen;

/// Runtime system with GC, closures, and bytecode interpretation.
#[cfg(feature = "runtime")]
pub use oxilean_runtime as runtime;

/// Standard library (Nat, Bool, List, etc.).
#[cfg(feature = "std-lib")]
pub use oxilean_std as std_lib;

/// Static analysis and lint rules.
#[cfg(feature = "lint")]
pub use oxilean_lint as lint;

/// Build system with incremental compilation.
#[cfg(feature = "build-sys")]
pub use oxilean_build as build_sys;

/// WebAssembly support.
#[cfg(feature = "wasm")]
pub use oxilean_wasm as wasm;