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.

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

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

Trampolining

Deep ordinary data is represented by generated VDescCon values. Conversion stays structural except for explicitly documented eta/unfolding rules.

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.

admitLevel

admitLevel: is a Level term-independent? — every normLevel summand rests on a zero or empty-spine var base; the shared predicate behind every universe-level soundness gate. Rejects applied-neutral bases, admits level variables.

admitLevel : Val -> Bool

cPeelArm

cPeelArm: deep-arm classifier for cPeel — peels VNe spines and VMu/VDesc/VBootEq towers onto the machine frontier via the shared elimGoals decomposition. Returns a layer record or null.

cPeelArm : Depth -> Val -> Val -> ({ kind; goals; na; nb; nd; } | null)

cPeelBinder

cPeelBinder: binder-arm classifier for cPeel — mirrors convStep's VPi/VLam/eta/VSigma arms (and the preceding Lift-collapse guard) so binder layers peel flat. Returns a layer record or null.

cPeelBinder : Depth -> Val -> Val -> ({ kind; goals; na; nb; nd; } | null)

conv

conv: definitional equality on values at binding depth — purely structural with Σ/Unit/Π-eta; foundation of Sub in check and the kernel TCB.

conv : Depth -> Val -> Val -> Bool

convElim

convElim: elimination-frame equality at binding depth — same tag and recursively conv on every carried value; building block of convSp.

convElim : Depth -> Elim -> Elim -> Bool

convLevel

convLevel: definitional equality on Level expressions — normLevel both sides, then structural compare; required because convLevel is non-trivial under levelMax associativity.

convLevel : Val -> Val -> Bool

convSp

convSp: spine equality at binding depth — same length plus pairwise convElim on each frame; used to compare two neutral-value spines.

convSp : Depth -> Spine -> Spine -> Bool

convStep

convStep: single conversion step over forced values — the conv dispatch body, called by the runConvF machine for non-structural goals.

convStep : Depth -> Val -> Val -> Bool

normLevel

normLevel: normalise a Level expression to canonical form — levelMax/levelSuc collapsed via the algebraic laws so two equivalent forms compare equal under convLevel.

normLevel : Val -> Val