Conv

Checks whether two values are definitionally equal at a given binding depth. Purely structural — no type information used, no eta expansion. Pure function — part of the TCB.

Spec reference: kernel-spec.md §6.

Core Functions

• conv : Depth → Val → Val → Bool — check definitional equality.
• convSp : Depth → Spine → Spine → Bool — check spine equality (same length, pairwise convElim).
• convElim : Depth → Elim → Elim → Bool — check elimination frame equality (same tag, recursively conv on carried values).

Conversion Rules

• §6.1 Structural: same-constructor values with matching fields. Universe levels compared by ==. Primitive literals by value.
• §6.2 Binding forms: Pi, Lam, Sigma compared under a fresh variable at depth d (instantiate both closures, compare at d+1).
• §6.3 Compound values: recursive on all components.
• §6.4 Neutrals: same head level and convertible spines.
• §6.5 Catch-all: different constructors → false.

Trampolining

VSucc and VCons chains use genericClosure to avoid stack overflow on S^5000 or cons^5000 comparisons.

No Eta

conv does not perform eta expansion: a neutral f and λx. f(x) are not definitionally equal. Cumulativity (U(i) ≤ U(j)) is handled in check.nix, not here.