Value

Values are the semantic domain produced by evaluation. They use de Bruijn levels (counting outward from the top of the context), not indices, which makes weakening trivial.

Spec reference: kernel-spec.md §3.

Closures

mkClosure : Env → Tm → Closure — defunctionalized closure. No Nix lambdas in the TCB; a closure is { env, body } where body is a kernel Tm evaluated by eval.instantiate.

Value Constructors

Each v* constructor mirrors a term constructor:

• vLam, vPi — function values/types (carry name, domain, closure)
• vSigma, vPair — pair types/values
• vNat, vZero, vSucc — natural number values
• vBool, vTrue, vFalse — boolean values
• vList, vNil, vCons — list values
• vUnit, vTt — unit
• vVoid — empty type
• vSum, vInl, vInr — sum values
• vEq, vRefl — identity values
• vU — universe values
• vString, vInt, vFloat, vAttrs, vPath, vFunction, vAny — primitive types
• vStringLit, vIntLit, vFloatLit, vAttrsLit, vPathLit, vFnLit, vAnyLit — primitive literals

Neutrals

vNe : Level → Spine → Val — a stuck computation: a variable (identified by de Bruijn level) applied to a spine of eliminators.

freshVar : Depth → Val — neutral with empty spine at the given depth. Used during type-checking to introduce fresh variables under binders.

Elimination Frames (Spine Entries)

• eApp, eFst, eSnd — function/pair eliminators
• eNatElim, eBoolElim, eListElim, eAbsurd, eSumElim, eJ — inductive eliminators