Skip to main content

Crate oxilean_std

Crate oxilean_std 

Source
Expand description

§OxiLean Standard Library — Core Data Types & Theorems

The standard library provides essential types, type classes, and theorems for OxiLean programs. It is written in OxiLean itself and loaded into the kernel environment at startup.

§Architecture Overview

The standard library is organized into logical categories:

  • Primitive Types: nat, bool, char, int, string, list, array, option, result
  • Type Classes: Eq, Ord, Show, Repr, Functor, Monad, Monoid, Decidable
  • Core Theorems: equality, logic, arithmetic, order
  • Utilities: tactic lemmas, decision procedures, parsing combinators

§Environment Building

Loading happens via build_*_env functions:

ⓘ
let env = Environment::new();
let env = build_nat_env(env)?;
let env = build_list_env(env)?;
let env = build_eq_env(env)?;

See registry module for module metadata and dependency graph.

Re-exports§

pub use algebra::build_algebra_env;
pub use array::build_array_env;
pub use bitvec::build_bitvec_env;
pub use bool::build_bool_env;
pub use category_theory::build_category_theory_env;
pub use char::build_char_env;
pub use decidable::build_decidable_env;
pub use either::build_either_env;
pub use eq::build_eq_env;
pub use fin::build_fin_env;
pub use functor::build_functor_env;
pub use group_theory::build_group_theory_env;
pub use hashmap::build_hashmap_env;
pub use hashset::build_hashset_env;
pub use int::build_int_env;
pub use io::build_io_env;
pub use lazy::build_lazy_env;
pub use list::build_list_env;
pub use logic::build_logic_env;
pub use monad::build_monad_env;
pub use nat::build_nat_env;
pub use option::build_option_env;
pub use ord::build_ord_env;
pub use order::build_order_env;
pub use ordering::build_ordering_env;
pub use parsec::build_parsec_env;
pub use prod::build_prod_env;
pub use prop::build_prop_env;
pub use quotient_types::build_quotient_types_env;
pub use range::build_range_env;
pub use rbtree::build_rbtree_env;
pub use real::build_real_env;
pub use repr::build_repr_env;
pub use result::build_result_env;
pub use set::build_set_env;
pub use show::build_show_env;
pub use sigma::build_sigma_env;
pub use stream::build_stream_env;
pub use string::build_string_env;
pub use sum::build_sum_env;
pub use tactic_lemmas::build_tactic_lemmas_env;
pub use thunk::build_thunk_env;
pub use topology::build_topology_env;
pub use vec::build_vec_env;
pub use wellfounded::build_wellfounded_env;
pub use registry::all_modules;
pub use registry::all_theorems;
pub use registry::count_default_modules;
pub use registry::count_total_modules;
pub use registry::default_modules;
pub use registry::dependents_of;
pub use registry::direct_deps;
pub use registry::entries_in_module;
pub use registry::find_module;
pub use registry::lookup_std_entry;
pub use registry::module_category;
pub use registry::modules_for_phase;
pub use registry::topological_sort_modules;
pub use registry::BuildPhase;
pub use registry::ModuleDep;
pub use registry::StdCategory;
pub use registry::StdEntry;
pub use registry::StdFeatures;
pub use registry::StdLibStats;
pub use registry::StdModuleEntry;
pub use registry::StdVersion;
pub use registry::CORE_DEPS;
pub use registry::STD_KNOWN_ENTRIES;
pub use registry::STD_MODULE_REGISTRY;
pub use registry::STD_VERSION;
pub use std_utilities::BitSet64;
pub use std_utilities::Counter;
pub use std_utilities::Diagnostic;
pub use std_utilities::DiagnosticBag;
pub use std_utilities::DiagnosticLevel;
pub use std_utilities::DirectedGraph;
pub use std_utilities::FreshNameGen;
pub use std_utilities::Located;
pub use std_utilities::MinHeap;
pub use std_utilities::MultiMap;
pub use std_utilities::NameTable;
pub use std_utilities::ScopeTable;
pub use std_utilities::Span;
pub use std_utilities::StringSet;
pub use std_utilities::Trie;

Modules§

abstract_algebra_adv
Auto-generated module structure
abstract_algebra_advanced
Auto-generated module structure
abstract_interpretation
Auto-generated module structure
abstract_rewriting
Abstract Rewriting Systems (ARS) and term rewriting.
algebra
Auto-generated module structure
algebraic_combinatorics
Algebraic combinatorics: Young tableaux, symmetric functions, crystal graphs, Robinson-Schensted correspondence, and combinatorial sequences.
algebraic_effects
Auto-generated module structure
algebraic_geometry
Auto-generated module structure
algebraic_k_theory
Algebraic K-theory: K_0, K_1, and K_2 groups for rings and fields.
algebraic_number_theory
Auto-generated module structure
algebraic_topology
Auto-generated module structure
analytic_number_theory
Auto-generated module structure
approximation_algorithms
Auto-generated module structure
arithmetic_geometry
Auto-generated module structure
array
Auto-generated module structure
automata_theory
Auto-generated module structure
bayesian_networks
Auto-generated module structure
bioinformatics
Auto-generated module structure
birational_geometry
Auto-generated module structure
bitvec
Auto-generated module structure
bool
Auto-generated module structure
categorical_logic
Auto-generated module structure
category_theory
Auto-generated module structure
category_theory_ext
Auto-generated module structure
certified_algorithms
Auto-generated module structure
chaos_theory
Auto-generated module structure
char
Auto-generated module structure
chromatic_homotopy
Auto-generated module structure
coalgebra_theory
Auto-generated module structure
coding_theory
Auto-generated module structure
coinduction
Coinductive proofs and greatest fixed points.
combinatorial_game_theory
Auto-generated module structure
combinatorial_optimization
Auto-generated module structure
combinatorics
Auto-generated module structure
combinatory_logic
Combinatory logic and SKI calculus.
compiler_theory
Auto-generated module structure
complex
Auto-generated module structure
complexity
Auto-generated module structure
computability_theory
Computability and decidability theory.
computational_geometry
Auto-generated module structure
concurrency_theory
Auto-generated module structure
constructive_mathematics
Auto-generated module structure
control_theory
Auto-generated module structure
convex_analysis
Convex analysis module.
convex_geometry
Auto-generated module structure
convex_optimization
Auto-generated module structure
cryptographic_protocols
Auto-generated module structure
cryptography
Auto-generated module structure
cubical_type_theory
Auto-generated module structure
data_structures
Auto-generated module structure
decidable
Auto-generated module structure
denotational_semantics
Auto-generated module structure
dependent_type_theory
Dependent type theory formalizations.
derived_algebraic_geometry
Auto-generated module structure
descriptive_set_theory
Auto-generated module structure
differential_equations
Auto-generated module structure
differential_geometry
Auto-generated module structure
differential_privacy
Auto-generated module structure
diophantine_geometry
Auto-generated module structure
distributed_systems_theory
Auto-generated module structure
domain_theory
Auto-generated module structure
either
Auto-generated module structure
elliptic_curves
Auto-generated module structure
env_builder
Auto-generated module structure
eq
Auto-generated module structure
ergodic_theory
Auto-generated module structure
fin
Auto-generated module structure
finite_element_method
Auto-generated module structure
forcing_theory
Auto-generated module structure
formal_argumentation
Formal Argumentation — Dung’s abstract argumentation frameworks.
formal_epistemology
Formal Epistemology — belief revision, epistemic logic, Kripke semantics.
formal_languages
Auto-generated module structure
formal_verification
Auto-generated module structure
functional_analysis
Auto-generated module structure
functional_calculus
Auto-generated module structure
functional_programming
Auto-generated module structure
functor
Auto-generated module structure
fuzzy_logic
Auto-generated module structure
game_theory
Auto-generated module structure
game_theory_ext
Auto-generated module structure
geometric_group_theory
Auto-generated module structure
geometric_measure_theory
Auto-generated module structure
geometric_topology
Geometric topology: 3-manifolds, knot surgery, JSJ decomposition, gluing matrices.
graph
Auto-generated module structure
graph_algorithms
Advanced graph algorithms module.
groebner_bases
Auto-generated module structure
group_theory
Auto-generated module structure
harmonic_analysis
Auto-generated module structure
hashmap
Auto-generated module structure
hashset
Auto-generated module structure
higher_category_theory
Auto-generated module structure
homological_algebra
Auto-generated module structure
homological_computations
Auto-generated module structure
homotopy_theory
Auto-generated module structure
homotopy_type_theory
Auto-generated module structure
hybrid_systems
Hybrid dynamical systems theory.
information_geometry
Auto-generated module structure
information_theoretic_security
Auto-generated module structure
information_theory
Auto-generated module structure
information_theory_ext
Auto-generated module structure
int
Auto-generated module structure
intersection_theory
Auto-generated module structure
io
Auto-generated module structure
iwasawa_theory
Auto-generated module structure
k_theory
Auto-generated module structure
knot_theory
Auto-generated module structure
lambda_calculus
Auto-generated module structure
lattice_theory
Auto-generated module structure
lazy
Auto-generated module structure
lie_theory
Auto-generated module structure
linear_algebra
Auto-generated module structure
linear_logic
Auto-generated module structure
linear_programming
Auto-generated module structure
linear_temporal_logic
Linear Temporal Logic (LTL) — model checking over Kripke structures.
list
Auto-generated module structure
logic
Auto-generated module structure
logic_programming
Prolog-style logic programming engine: SLD resolution, unification, databases.
low_dimensional_topology
Auto-generated module structure
machine_learning
Auto-generated module structure
mathematical_ecology
Auto-generated module structure
mathematical_physics
Auto-generated module structure
measure_theory
Auto-generated module structure
mechanism_design
Auto-generated module structure
modal_logic
Auto-generated module structure
model_checking
Auto-generated module structure
model_theory
Auto-generated module structure
modular_forms
Auto-generated module structure
monad
Auto-generated module structure
motivic_cohomology
Auto-generated module structure
nat
Auto-generated module structure
network_theory
Auto-generated module structure
noncommutative_geometry
Auto-generated module structure
nonlinear_dynamics
Nonlinear dynamics module.
nonstandard_analysis
Auto-generated module structure
number_theory
Auto-generated module structure
numerical_analysis
Auto-generated module structure
numerical_linear_algebra
Auto-generated module structure
observational_type_theory
Auto-generated module structure
operations_research
Auto-generated module structure
operator_algebras
Auto-generated module structure
optimal_transport
Optimal transport module.
optimization_theory
Auto-generated module structure
option
Auto-generated module structure
ord
Auto-generated module structure
order
Auto-generated module structure
order_topology
Auto-generated module structure
ordering
Auto-generated module structure
padic_analysis
Auto-generated module structure
padic_hodge_theory
Auto-generated module structure
parameterized_complexity
Auto-generated module structure
parametricity
Auto-generated module structure
parsec
Auto-generated module structure
pde_theory
Auto-generated module structure
persistent_data_structures
Persistent (immutable) data structures.
point_free_topology
Auto-generated module structure
point_set_topology
Auto-generated module structure
post_quantum_crypto
Auto-generated module structure
probabilistic_programming
Auto-generated module structure
probability
Auto-generated module structure
prod
Auto-generated module structure
program_extraction
Program extraction from constructive proofs via the Curry-Howard correspondence.
program_logics
Auto-generated module structure
program_synthesis
Auto-generated module structure
proof_mining
Auto-generated module structure
proof_theory
Auto-generated module structure
prop
Auto-generated module structure
quantum_computing
Auto-generated module structure
quantum_error_correction
Auto-generated module structure
quantum_field_theory
Auto-generated module structure
quantum_information
Auto-generated module structure
quotient_types
Auto-generated module structure
ramsey_theory
Ramsey theory module.
random_matrix_theory
Auto-generated module structure
range
Auto-generated module structure
rbtree
Auto-generated module structure
real
Auto-generated module structure
registry
Standard library module registry, dependency graph, feature flags, and metadata types.
repr
Auto-generated module structure
representation_theory
Auto-generated module structure
result
Auto-generated module structure
reverse_mathematics
Auto-generated module structure
rough_set_theory
Auto-generated module structure
session_types
Auto-generated module structure
set
Auto-generated module structure
set_theory_zfc
Auto-generated module structure
sheaf_theory
Auto-generated module structure
show
Auto-generated module structure
sigma
Auto-generated module structure
social_choice_theory
Auto-generated module structure
spectral_graph_theory
Spectral graph theory module.
spectral_methods
Auto-generated module structure
spectral_theory
Auto-generated module structure
static_analysis
Auto-generated module structure
statistical_learning
Auto-generated module structure
statistical_mechanics
Auto-generated module structure
std_utilities
Extended standard library utility types: Span, Located, NameTable, DiagnosticLevel, Diagnostic, DiagnosticBag, ScopeTable, Counter, FreshNameGen, StringSet, MultiMap, Trie, BitSet64, MinHeap, DirectedGraph.
stochastic_control
Auto-generated module structure
stochastic_processes
Auto-generated module structure
stream
Auto-generated module structure
string
Auto-generated module structure
string_theory_basics
Auto-generated module structure
sum
Auto-generated module structure
surreal_numbers
Auto-generated module structure
symplectic_geometry
Auto-generated module structure
systems_biology
Auto-generated module structure
tactic_lemmas
Auto-generated module structure
tauberian_theory
Auto-generated module structure
temporal_logic
Auto-generated module structure
term_rewriting
Auto-generated module structure
thunk
Auto-generated module structure
topological_data_analysis
Auto-generated module structure
topological_quantum_computation
Auto-generated module structure
topology
Auto-generated module structure
topology_ext
Auto-generated module structure
topos_theory
Auto-generated module structure
tropical_geometry
Auto-generated module structure
type_directed_search
Hoogle-like type-directed function search.
type_inference_algorithms
Auto-generated module structure
type_theory
Auto-generated module structure
type_theory_advanced
Auto-generated module structure
universal_algebra
Auto-generated module structure
variational_analysis
Auto-generated module structure
variational_calculus
Auto-generated module structure
vec
Auto-generated module structure
wellfounded
Auto-generated module structure
zero_knowledge_proofs
Zero-knowledge proofs module.