# _encoders


Kernel-Tm and Val-level encoders for surface description combinators; consumed by `tc/eval` (descDescVal) and `tc/generic` (encodeDescXTm pre-evaluations).

## `__descDesc`

___descDesc: private internal-use alias for `descDesc` — exposed for the encoder cascade; surface code should use `descDesc`._

```
__descDesc : Hoas -> Level -> Hoas
```

## `descDescApp`

_descDescApp: applied `descDesc` form — `descDescApp I k` produces `descDesc I k` as a closed Tm; convenience for sites that need the pre-applied form._

```
descDescApp : Hoas -> Level -> Hoas
```

## `descDescAppAtI`

_descDescAppAtI: applied `descDesc` form with explicit index-universe level — `descDescAppAtI iLev I k` evaluates to a canonical stamp with params `[iLev, I, k]`._

```
descDescAppAtI : Level -> Hoas -> Level -> Hoas
```

## `descDescTm`

_descDescTm: pre-elaborated `descDesc` term — closed kernel `Tm` form usable directly by kernel rules that need the description-of-descriptions without re-elaborating._

```
descDescTm : Tm
```

## `descDescVal`

_descDescVal: pre-evaluated `descDesc` value — the kernel `Val` form, ready for `interpD` / `descInd` consumption without re-evaluation._

```
descDescVal : Val
```

## `encodeDescArg`

_encodeDescArg: HOAS encoder for `descArg` — `encodeDescArg I k S T` builds the structural encoding of a `descArg I k S T` description._

```
encodeDescArg : Hoas -> Level -> Hoas -> Hoas -> Hoas
```

## `encodeDescArgAt`

_encodeDescArgAt: HOAS encoder for `descArgAt` — universe-polymorphic encoder for `descArgAt I l k S T`._

```
encodeDescArgAt : Hoas -> Level -> Level -> Hoas -> Hoas -> Hoas
```

## `encodeDescArgAtTm`

_encodeDescArgAtTm: pre-elaborated `encodeDescArgAt` — closed kernel `Tm`._

```
encodeDescArgAtTm : Tm
```

## `encodeDescArgTm`

_encodeDescArgTm: pre-elaborated `encodeDescArg` — closed kernel `Tm`._

```
encodeDescArgTm : Tm
```

## `encodeDescElim`

_encodeDescElim: HOAS encoder for `descElim` — produces the cascade application that walks `descDesc`'s plus-tree to dispatch on a `VDescCon` value's constructor._

```
encodeDescElim : Hoas -> Level -> Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas
```

## `encodeDescElimTm`

_encodeDescElimTm: pre-elaborated `encodeDescElim` — closed kernel `Tm` form of the eliminator cascade._

```
encodeDescElimTm : Tm
```

## `encodeDescElimVal`

_encodeDescElimVal: pre-evaluated `encodeDescElim` — kernel `Val` form, ready for direct consumption without re-evaluation._

```
encodeDescElimVal : Val
```

## `encodeDescPi`

_encodeDescPi: HOAS encoder for `piI` — `encodeDescPi I k S f D` builds the structural encoding of a `piI I k S f D` description._

```
encodeDescPi : Hoas -> Level -> Hoas -> Hoas -> Hoas -> Hoas
```

## `encodeDescPiAt`

_encodeDescPiAt: HOAS encoder for `piIAt` — universe-polymorphic encoder for `piIAt I l k S f D`._

```
encodeDescPiAt : Hoas -> Level -> Level -> Hoas -> Hoas -> Hoas -> Hoas
```

## `encodeDescPiAtTm`

_encodeDescPiAtTm: pre-elaborated `encodeDescPiAt` — closed kernel `Tm`._

```
encodeDescPiAtTm : Tm
```

## `encodeDescPiTm`

_encodeDescPiTm: pre-elaborated `encodeDescPi` — closed kernel `Tm`._

```
encodeDescPiTm : Tm
```

## `encodeDescPlus`

_encodeDescPlus: HOAS encoder for `plusI` — `encodeDescPlus I k A B` builds the structural encoding of a `plusI I k A B` description._

```
encodeDescPlus : Hoas -> Level -> Hoas -> Hoas -> Hoas
```

## `encodeDescPlusTm`

_encodeDescPlusTm: pre-elaborated `encodeDescPlus` — closed kernel `Tm`._

```
encodeDescPlusTm : Tm
```

## `encodeDescRec`

_encodeDescRec: HOAS encoder for `recI` — `encodeDescRec I k j D` builds the structural encoding of a `recI I k j D` description._

```
encodeDescRec : Hoas -> Level -> Hoas -> Hoas -> Hoas
```

## `encodeDescRecTm`

_encodeDescRecTm: pre-elaborated `encodeDescRec` — closed kernel `Tm`._

```
encodeDescRecTm : Tm
```

## `encodeDescRet`

_encodeDescRet: HOAS encoder for `retI` — `encodeDescRet I k j` builds the `μ ⊤ (descDesc I k) tt` value structurally encoding a `retI I k j` description._

```
encodeDescRet : Hoas -> Level -> Hoas -> Hoas  -- I, k, targetIdx
```

## `encodeDescRetTm`

_encodeDescRetTm: pre-elaborated `encodeDescRet` — closed kernel `Tm` lambda; consumed by `interpD`'s encoded-desc view branch._

```
encodeDescRetTm : Tm
```

## `natDescTm`

_natDescTm: pre-elaborated `Nat` description term — closed kernel `Tm` encoding `natDesc`; used by the kernel where the HOAS form would re-elaborate._

```
natDescTm : Tm
```