# Term Syntax of the kernel's term language. All 48 constructors produce attrsets with a `tag` field (not `_tag`, to distinguish kernel terms from effect system nodes). Binding is de Bruijn indexed: `mkVar i` refers to the i-th enclosing binder (0 = innermost). Name annotations (`name` parameter on `mkPi`, `mkLam`, `mkSigma`, `mkLet`) are cosmetic — used only in error messages, never in equality checking. ## Constructors ### Variables and Binding - `mkVar : Int → Tm` — variable by de Bruijn index - `mkLet : String → Tm → Tm → Tm → Tm` — `let name : type = val in body` - `mkAnn : Tm → Tm → Tm` — type annotation `(term : type)` ### Functions - `mkPi : String → Tm → Tm → Tm` — dependent function type `Π(name : domain). codomain` - `mkLam : String → Tm → Tm → Tm` — lambda `λ(name : domain). body` - `mkApp : Tm → Tm → Tm` — application `fn arg` ### Pairs - `mkSigma : String → Tm → Tm → Tm` — dependent pair type `Σ(name : fst). snd` - `mkPair : Tm → Tm → Tm` — pair constructor `(fst, snd)` - `mkFst : Tm → Tm` — first projection - `mkSnd : Tm → Tm` — second projection ### Inductive Types - `mkUnit`, `mkTt` — unit type and value - `mkBootSum`, `mkBootInl`, `mkBootInr`, `mkBootSumElim` — bootstrap coproduct for `descPlus` - `mkBootEq`, `mkBootRefl`, `mkBootJ` — identity type with J eliminator ### Universes - `mkU : (Int | Tm) → Tm` — universe `U(level)`. Accepts either a concrete Int (wrapped via `mkLevelLit`) or a Level-typed Tm directly. - `mkLevelLit : Int → Tm` — builds `suc^n zero` as a Level term. ### Axiomatized Primitives - `mkString`, `mkInt`, `mkFloat`, `mkAttrs`, `mkPath`, `mkDerivation`, `mkFunction`, `mkAny` — type formers - `mkStringLit`, `mkIntLit`, `mkFloatLit`, `mkAttrsLit`, `mkPathLit`, `mkDerivationLit`, `mkFnLit`, `mkAnyLit` — literal values ## `funextTypeTm` _funextTypeTm: pre-elaborated kernel term for the funext axiom's type `∀(j,k,A,B,f,g). (∀a. Eq (B a) (f a) (g a)) -> Eq (Π a:A. B a) f g`._ ## `mkAbsurd` _mkAbsurd: empty-type eliminator — `absurd P x` discharges a stuck `x : Empty` to produce a value of any type `P`; well-typed only when `x` is a neutral (Empty has no canonical inhabitants)._ ``` mkAbsurd : Tm -> Tm -> Tm -- type (P), term (x : Empty) ``` ## `mkAllD` _mkAllD: induction-hypothesis collector `All D X P i payload` — given motive `P : (i:I) -> X i -> U(k)`, threads `P` through every recursive child in the payload._ ``` mkAllD : Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm -- k, I, D, level, X, P, i, payload ``` ## `mkAnn` _mkAnn: type annotation `(term : type)` — fixes the checking direction at the kernel level; consumed by `Sub` and elaboration._ ``` mkAnn : Tm -> Tm -> Tm -- term, type ``` ## `mkAnnTrusted` _mkAnnTrusted: type annotation marked as elaborator-trusted — `check` skips re-validation of `term` against `type` since elaboration has already proved well-typedness._ ``` mkAnnTrusted : Tm -> Tm -> Tm -- term, type ``` ## `mkAnnTrustedWithDescRef` _mkAnnTrustedWithDescRef: trusted annotation carrying a `_descRef` sidecar — used by the HOAS elaborator to retain levitated description provenance across eval/quote round-trips._ ``` mkAnnTrustedWithDescRef : Tm -> Tm -> Any -> Tm -- term, type, descRef ``` ## `mkAnnTrustedWithLabels` _mkAnnTrustedWithLabels: trusted annotation carrying `_label` / `_conLabel` sidecars — used by `H.withDescLabel` / `H.withConLabel` to surface presentation labels on `descView`._ ``` mkAnnTrustedWithLabels : Tm -> Tm -> { label?, conLabel? } -> Tm ``` ## `mkAny` _mkAny: axiomatised top primitive type `Any` — accepts every Nix value; used as the lossy-fallback kernel for approximate types._ ## `mkAnyLit` _mkAnyLit: kernel literal for an arbitrary Nix value `v : Any` — used by approximate types whose kernel slot is `mkAny`._ ``` mkAnyLit : Any -> Tm ``` ## `mkApp` _mkApp: function application `fn arg` — head `fn` is checked first to infer Π type, then `arg` is checked against the domain._ ``` mkApp : Tm -> Tm -> Tm -- fn, arg ``` ## `mkAttrs` _mkAttrs: axiomatised primitive type `Attrs` — type former at U(0) inhabited by any Nix attribute set, including `{}`._ ## `mkAttrsLit` _mkAttrsLit: kernel literal for a Nix attribute set `a : Attrs`; the attrs are carried opaquely (no per-field validation at the kernel level)._ ``` mkAttrsLit : Attrs -> Tm ``` ## `mkBootEq` _mkBootEq: bootstrap identity type `Eq(A, a, b)` — propositional equality used by `descRet`'s level transport and by the J eliminator._ ``` mkBootEq : Tm -> Tm -> Tm -> Tm -- A, a, b ``` ## `mkBootInl` _mkBootInl: left-injection of `mkBootSum` — `inl(a) : A + B`; carries both `A` and `B` for elaboration shape recovery._ ``` mkBootInl : Tm -> Tm -> Tm -> Tm -- leftTy, rightTy, value ``` ## `mkBootInr` _mkBootInr: right-injection of `mkBootSum` — `inr(b) : A + B`; carries both `A` and `B` for elaboration shape recovery._ ``` mkBootInr : Tm -> Tm -> Tm -> Tm -- leftTy, rightTy, value ``` ## `mkBootJ` _mkBootJ: J eliminator on `mkBootEq` — transports a property `motive` along a proof of equality, yielding a term at the other endpoint._ ``` mkBootJ : Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm -- A, a, motive, identity, b, eq ``` ## `mkBootRefl` _mkBootRefl: bootstrap reflexivity `refl : Eq(A, a, a)` — the canonical inhabitant of every reflexive identity type; check-mode only at elaboration._ ## `mkBootSum` _mkBootSum: bootstrap coproduct type `A + B` — used by `descPlus` to encode sum-of-descriptions before generic sums become available._ ``` mkBootSum : Tm -> Tm -> Tm -- left, right ``` ## `mkBootSumElim` _mkBootSumElim: bootstrap sum eliminator — case-splits a `A + B` scrutinee through `onLeft`/`onRight` arms at motive `(_:A+B) -> Q _`._ ``` mkBootSumElim : Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm -- leftTy, rightTy, motive, onLeft, onRight, scrut ``` ## `mkCanonApp` _mkCanonApp: generic identity-tagged application — `canon-app id params body` evaluates by currying-applying `body` to `params` and stamps the result `VDescCon` with `_canonRef = { id; params; }`; conv/quote short-circuit on the canonical identity instead of forcing `.D`._ ``` mkCanonApp : String -> [Tm] -> Tm -> Tm -- id, params, body ``` ## `mkDerivation` _mkDerivation: axiomatised primitive type `Derivation` — type former at U(0) inhabited by Nix derivation values (attrsets with `type = "derivation"`); the irreducible Nix-store-producing value category._ ## `mkDerivationLit` _mkDerivationLit: kernel literal for a Nix derivation `d : Derivation`; the value is carried opaquely (kernel never inspects derivation attrs)._ ``` mkDerivationLit : Derivation -> Tm ``` ## `mkDesc` _mkDesc: level-zero description type `Desc I k` at index sort `I : U(0)` and universe level `k` — the levitated algebra of constructors for datatypes._ ``` mkDesc : Tm -> Tm -> Tm -- k, I ``` ## `mkDescAt` _mkDescAt: `Desc^k I` carrying an explicit `iLev` for the universe of `I`. The kernel synthesises the desc-formation level as `U(suc (max k iLev))`._ ``` mkDescAt : Tm -> Tm -> Tm -> Tm -- iLev, k, I ``` ## `mkDescCon` _mkDescCon: constructor introduction for `μ I D i` — takes a payload typed by `interpD D (μ I D) i` and returns the corresponding `μ` value._ ``` mkDescCon : Tm -> Tm -> Tm -> Tm -- D, i, payload ``` ## `mkDescConChain` _mkDescConChain: flat-form linear-chain dual of an N-deep mkDescCon. `layers` is a flat outer-first Nix-list of `{ i; heads }` records; `base = { D; i; d }` at the terminator. The consumer pass-graph (evalF, conv, extract, quote) walks the list iteratively, so libnix `forceValueDeep` depth is O(1) regardless of N. Bijective dual of the chain-form Val (`_shape == "linearChain"`)._ ``` mkDescConChain : { layers : [{i:Tm; heads:[Tm]}]; base : {D:Tm; i:Tm; d:Tm}; outerD : Tm; payloadTag : String; payloadLeft : Tm; payloadRight : Tm; } -> Tm ``` ## `mkDescConWithCert` _mkDescConWithCert: `mkDescCon` carrying a `Squash`-truncated guard certificate — threads a refinement guard's decision proof through the kernel for description-backed Record/Variant constructors (`descConCertified`)._ ``` mkDescConWithCert : Tm -> Tm -> Tm -> Tm -> Tm -- D, i, payload, cert ``` ## `mkDescDescApp` _mkDescDescApp: level-zero applied form of `descDesc` — `Desc^(suc L) ⊤` whose mu-fixpoint is `Desc^L I` for `I : U(0)`; bootstraps generic programming over descriptions themselves._ ``` mkDescDescApp : Tm -> Tm -> Tm -- I, L ``` ## `mkDescDescAppAt` _mkDescDescAppAt: applied form of `descDesc` carrying an explicit `ℓ` for the universe of `I` — generalised outer signature `λℓ:Level. λI:U(ℓ). λL:Level. Desc^(suc (max L ℓ)) ⊤`._ ``` mkDescDescAppAt : Tm -> Tm -> Tm -> Tm -- ℓ, I, L ``` ## `mkDescInd` _mkDescInd: levitated induction principle on `μ I D` — given a motive and step function, produces a generic recursor over the data described by `D`._ ``` mkDescInd : Tm -> Tm -> Tm -> Tm -> Tm -> Tm -- I, D, motive, step, scrut ``` ## `mkEmpty` _mkEmpty: empty type `Empty` — initial type at universe level 0; no constructors._ ## `mkEverywhereD` _mkEverywhereD: payload-traversal combinator over a description — applies a per-node `f` at every recursive position, producing a derived payload of the same shape._ ``` mkEverywhereD : Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm ``` ## `mkFloat` _mkFloat: axiomatised primitive type `Float` — type former at U(0) inhabited by Nix floats (excludes integers)._ ## `mkFloatLit` _mkFloatLit: kernel literal for a Nix float `x : Float`._ ``` mkFloatLit : Float -> Tm ``` ## `mkFnLit` _mkFnLit: kernel literal for an opaque Nix function `f : Function` — wraps the function in an `fnBox` for thunk-identity-preserving conversion._ ``` mkFnLit : Function -> Tm ``` ## `mkFst` _mkFst: first-projection eliminator on a Σ-typed term — yields the dependent `fst` component; Σ-eta is exercised in `conv`._ ``` mkFst : Tm -> Tm ``` ## `mkFunction` _mkFunction: axiomatised primitive type `Function` — type former at U(0) inhabited by opaque Nix-level functions wrapped via `mkOpaqueLam`._ ## `mkFunext` _mkFunext: function-extensionality axiom — given pointwise-equal `f`, `g` at every argument, produces an equality proof `Eq (Π a:A. B a) f g`._ ``` mkFunext : Tm -> Tm -> Tm -> Tm -> Tm -> Tm -- A, B, f, g, hypothesis ``` ## `mkInt` _mkInt: axiomatised primitive type `Int` — type former at U(0) inhabited by Nix integers (excludes floats)._ ## `mkIntEq` _mkIntEq: host `==` on `Int` literals `intEq a b : Bool` (parallel to `mkStrEq`)._ ``` mkIntEq : Tm -> Tm -> Tm -- a, b ``` ## `mkIntLe` _mkIntLe: host `<=` on `Int` literals `intLe a b : Bool` (parallel to `mkStrEq`). Non-symmetric — operand order preserved on a neutral spine._ ``` mkIntLe : Tm -> Tm -> Tm -- a, b ``` ## `mkIntLit` _mkIntLit: kernel literal for a Nix integer `n : Int`._ ``` mkIntLit : Int -> Tm ``` ## `mkInterpD` _mkInterpD: interpret a description `D : Desc I k` against a recursive carrier `X : I -> U(k)` at index `i`, yielding the payload type `interpD D X i`._ ``` mkInterpD : Tm -> Tm -> Tm -> Tm -> Tm -- k, I, D, X, i ``` ## `mkLam` _mkLam: lambda abstraction `λ(name : domain). body` — domain annotation is optional at check time (overridden by expected Π's domain)._ ``` mkLam : String -> Tm -> Tm -> Tm -- name, domain, body ``` ## `mkLet` _mkLet: let-binding `let name : type = val in body` — `name` is cosmetic, the binder is introduced into body's de Bruijn context as index `0`._ ``` mkLet : String -> Tm -> Tm -> Tm -> Tm -- name, type, val, body ``` ## `mkLevel` _mkLevel: universe-level sort `Level : U(0)` — the type former whose inhabitants are level expressions used in `mkU`._ ## `mkLevelLit` _mkLevelLit: concrete Level literal from an `Int` — builds `suc^n zero` as a Level term; entry point for level-polymorphism-free code._ ``` mkLevelLit : Int -> Tm ``` ## `mkLevelMax` _mkLevelMax: pointwise max of two levels `max(l, r) : Level` — used to compute the universe of `Σ` / `Π` types whose components inhabit distinct universes._ ``` mkLevelMax : Tm -> Tm -> Tm -- l, r ``` ## `mkLevelSuc` _mkLevelSuc: successor `suc(level) : Level` — increment a Level expression by one._ ``` mkLevelSuc : Tm -> Tm ``` ## `mkLevelZero` _mkLevelZero: level-zero literal `0 : Level` — base case of `Level`'s inductive structure._ ## `mkLift` _mkLift: Tarski lift `LiftAt l m A : U(m)` with `l ≤ m` — non-cumulative cross-level transport of a type at level `l` into level `m`._ ``` mkLift : Tm -> Tm -> Tm -> Tm -- l, m, A ``` ## `mkLiftElim` _mkLiftElim: elimination of `Lift l m A` — lowers a lifted term back to its original level; the inverse pairing with `mkLiftIntro`._ ``` mkLiftElim : Tm -> Tm -> Tm -> Tm -> Tm -- l, m, A, x ``` ## `mkLiftIntro` _mkLiftIntro: introduction of `Lift l m A` — lifts a term `a : A` at level `l` to a term at level `m`; eq witness is auto-emitted via `mkBootRefl`._ ``` mkLiftIntro : Tm -> Tm -> Tm -> Tm -> Tm -- l, m, A, a ``` ## `mkLitVal` _mkLitVal: closed-Val splice — opaque Val carrier whose eval is identity on the carried value. O(1) Val→Tm reflection; sound iff val is closed._ ``` mkLitVal : Val -> Tm ``` ## `mkMu` _mkMu: levitated fixpoint `μ I D i` — carrier type of values whose constructors are described by `D : Desc I k` at index `i`._ ``` mkMu : Tm -> Tm -> Tm -> Tm -- I, D, i ``` ## `mkOpaqueLam` _mkOpaqueLam: lambda over an opaque Nix function — kernel never inspects or applies it; `fnBox` thunk identity preserves conv reflexivity across eval/quote rounds._ ``` mkOpaqueLam : FnBox -> Tm -> Tm -- fnBox, piType ``` ## `mkPair` _mkPair: pair constructor `(fst, snd)` — both components are checked against the corresponding Σ slots at the expected type._ ``` mkPair : Tm -> Tm -> Tm -- fst, snd ``` ## `mkPath` _mkPath: axiomatised primitive type `Path` — type former at U(0) inhabited by Nix path values._ ## `mkPathLit` _mkPathLit: kernel literal for a Nix path `p : Path`._ ``` mkPathLit : Path -> Tm ``` ## `mkPi` _mkPi: dependent function type `Π(name : domain). codomain` — `name` is cosmetic, the binder is introduced into codomain's de Bruijn context as index `0`._ ``` mkPi : String -> Tm -> Tm -> Tm -- name, domain, codomain ``` ## `mkSigma` _mkSigma: dependent pair type `Σ(name : fst). snd` — `name` is cosmetic, the binder is introduced into snd's de Bruijn context as index `0`._ ``` mkSigma : String -> Tm -> Tm -> Tm -- name, fst, snd ``` ## `mkSnd` _mkSnd: second-projection eliminator on a Σ-typed term — yields the `snd` component with `fst` substituted; Σ-eta is exercised in `conv`._ ``` mkSnd : Tm -> Tm ``` ## `mkSquash` _mkSquash: propositional truncation `Squash A` — quotient of `A` collapsing all inhabitants to one, used for proof-irrelevant fields._ ``` mkSquash : Tm -> Tm ``` ## `mkSquashElim` _mkSquashElim: eliminator for `Squash` restricted to `Squash`-typed motives — preserves proof irrelevance by forbidding motives that distinguish inhabitants._ ``` mkSquashElim : Tm -> Tm -> Tm -> Tm -> Tm -- A, motive, fn, scrut ``` ## `mkSquashIntro` _mkSquashIntro: introduction of `Squash A` — lifts any `a : A` to a single inhabitant of `Squash A`._ ``` mkSquashIntro : Tm -> Tm ``` ## `mkStrEq` _mkStrEq: decidable equality on `String` literals `strEq a b : Bool` — used by indexed datatypes whose constructor selection branches on string keys._ ``` mkStrEq : Tm -> Tm -> Tm -- a, b ``` ## `mkStrLen` _mkStrLen: host string length `strLen s : Int` on a `String` literal; a stuck string operand keeps it neutral. Internalizes string-length refinements (e.g. non-emptiness)._ ``` mkStrLen : Tm -> Tm -- s ``` ## `mkString` _mkString: axiomatised primitive type `String` — type former at U(0) inhabited by Nix string values._ ## `mkStringLit` _mkStringLit: kernel literal for a Nix string `s : String`._ ``` mkStringLit : String -> Tm ``` ## `mkTt` _mkTt: unit value `tt` — sole inhabitant of `mkUnit`; eta-converts every term of type `Unit` to itself._ ## `mkU` _mkU: universe type `U(level)` at the given level expression — accepts either a concrete `Int` (wrapped via `mkLevelLit`) or a Level-typed `Tm`._ ``` mkU : (Int | Tm) -> Tm ``` ## `mkUnit` _mkUnit: unit type `Unit` — terminal type with single inhabitant `tt`; backs `fx.types.Unit` at universe level 0._ ## `mkVar` _mkVar: variable reference by de Bruijn index — `0` is the innermost binder; higher indices reach outer binders._ ``` mkVar : Int -> Tm ```