Module dag 

The kernel core: a type theory over a hash-consed expression DAG, in two modes (tc::Theory): Lean 4’s theory exactly, and LOGOS’s Calculus of Inductive Constructions.

This is the representation the kernel needs to be as fast as the fastest Lean kernels: de Bruijn indices, one id per structurally distinct term, loose-bound-variable ranges and free-variable flags cached per node, and every cache keyed on ids. In Lean’s theory it checks lean4export streams directly (export::check_export). In LOGOS’s it checks the declarations of a Context (logos_env::replay, logos_env::admit) with LOGOS’s own rules (logos_tc); LOGOS’s proof surfaces are still decided by the Term kernel and recheck, against which the core’s verdicts are locked.

Layout: name, level and expr are the interned stores; env the admitted declarations; tc inference, reduction and definitional equality by substitution, and sem the same judgment by evaluation into closures (Lean’s theory); check, inductive and primitive the admission rules; json and export the streaming reader; logos the lowering of LOGOS terms into the store, logos_tc LOGOS’s rules and logos_env its declarations; mirror keeps a core in step with a context through the context’s admission log.

Re-exports

pub use error::FailKind;

pub use error::KResult;

pub use error::KernelFailure;

pub use export::check_export;

pub use export::check_export_in;

pub use export::check_export_observed;

pub use export::check_export_sized;

pub use export::check_export_with;

pub use export::Verdict;

pub use tc::Kernel;

Modules

check

Admitting declarations: the kernel’s only door into the environment.

env

The environment: every declaration the kernel has admitted, indexed by name.

error

Typed kernel verdicts.

export

Reading a lean4export NDJSON stream straight into the kernel core.

expr

The kernel core’s expression store: a maximally shared DAG with de Bruijn indices.

inductive

Inductive families: Lean’s add_inductive, including nested-inductive elimination and recursor generation.

json

A small, allocation-free JSON reader for one NDJSON record at a time.

level

Universe levels: hash-consed, with a COMPLETE decision procedure for ≤ and ≡.

logos

LOGOS’s own terms in the core’s store: lower takes a Term of LOGOS’s Calculus of Inductive Constructions to an ExprId, and lift takes it back.

logos_env

A LOGOS context replayed into the core: every declaration, in dependency order, admitted by Theory::Logos’s checks, with the core’s verdict for each.

logos_tc

LOGOS’s Calculus of Inductive Constructions in the core: the rules Theory::Logos adds to the substitution checker.

mirror

The core beside a Context: a Kernel::logos per thread, kept in step with the context it last mirrored through that context’s admission log.

name

Hierarchical names, interned: Nat.succ is Str(Str(Anon, "Nat"), "succ"), and each distinct name is one NameId, so name equality is an integer compare.

nat

Lean’s natural numbers on top of logicaffeine_base::BigInt.

pretty

A bounded, readable rendering of core expressions for diagnostics.

primitive

Primitive validation: the literal extension is only as sound as the definitions it replaces.

primitive_wf

Validating the well-founded Nat primitives: Nat.div, Nat.mod, Nat.gcd, Nat.bitwise.

relevance

Argument relevance: which arguments of a definition cannot change what it computes.

sem

The value engine: type checking and definitional equality by evaluation into closures.

tc

Type inference, weak-head normalisation and definitional equality over the shared DAG.

wellknown

Names the kernel gives meaning to, interned once so every test is an id compare.