Quote

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

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

Linear VDescCon chains are quoted iteratively via genericClosure for O(1) stack depth on deep generated data (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.

lvl2Ix

lvl2Ix: convert a de Bruijn level to an index at binding depth — index = depth - level - 1; helper exposed for downstream tooling that interleaves with quotation.

lvl2Ix : Depth -> Level -> Index

nf

nf: normalise a term to its canonical form by eval then quote — useful for testing round-trip idempotency (nf env (nf env tm) == nf env tm).

nf : Env -> Tm -> Tm

quote

quote: read-back a value Val to a term Tm at binding depth — translates de Bruijn levels to indices via index = depth - level - 1. Pure TCB function.

quote : Depth -> Val -> Tm

quoteElim

quoteElim: quote a single elimination frame applied to a head term — dispatches on frame tag, recursively quoting each carried argument.

quoteElim : Depth -> Tm -> Elim -> Tm

quoteSp

quoteSp: quote a spine of elimination frames applied to a head term — folds left over the spine, calling quoteElim at each step.

quoteSp : Depth -> Tm -> Spine -> Tm