_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