# 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
```