Module tc 

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

The algorithm is Lean 4’s kernel algorithm — the one lean4lean transcribes from the C++ — so that every verdict agrees with Lean’s: lazy δ-reduction ordered by definitional height, proof irrelevance, η for functions and structures, unit-like types, K-like and structure recursor reduction, quotient reduction, and Nat/String literals. What differs is the representation underneath: structural equality is an id compare, and every cache is keyed on ids, so a subterm shared a thousand times is inferred, reduced and compared once.

Structs

Kernel

A kernel is plain data (its only shared cells are immutable: interned strings and admitted constants), so a clone is an independent kernel; mirror keeps one as a snapshot to branch from.

LocalDecl

Enums

Engine

The engine that checks declaration types and values (inductive families, quotients and the primitive validations always use the substitution checker).

Theory

The type theory a kernel checks.