Quote

Converts values back to terms, translating de Bruijn levels to indices. Pure function — part of the TCB.

Spec reference: kernel-spec.md §5.

Core Functions

• quote : Depth → Val → Tm — read back a value at binding depth d. Level-to-index conversion: index = depth - level - 1.
• quoteSp : Depth → Tm → Spine → Tm — quote a spine of eliminators applied to a head term (folds left over the spine).
• quoteElim : Depth → Tm → Elim → Tm — quote a single elimination frame applied to a head term.
• nf : Env → Tm → Tm — normalize: eval then quote. Useful for testing roundtrip idempotency (nf env (nf env tm) == nf env tm).
• lvl2Ix : Depth → Level → Index — level-to-index helper.

Trampolining

VSucc and VCons chains are quoted iteratively via genericClosure for O(1) stack depth on deep values (5000+ elements).

Binder Quotation

For VPi, VLam, VSigma: instantiates the closure with a fresh variable at the current depth, then quotes the body at depth + 1.