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.

Spec reference: kernel-spec.md §2.

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 (§2.2)

• 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 (§2.3)

• mkSigma : String → Tm → Tm → Tm — dependent pair type Σ(name : fst). snd
• mkPair : Tm → Tm → Tm → Tm — pair constructor (fst, snd) : ann
• mkFst : Tm → Tm — first projection
• mkSnd : Tm → Tm — second projection

Inductive Types

• mkNat, mkZero, mkSucc, mkNatElim — natural numbers with eliminator
• mkBool, mkTrue, mkFalse, mkBoolElim — booleans with eliminator
• mkList, mkNil, mkCons, mkListElim — lists with eliminator
• mkUnit, mkTt — unit type and value
• mkVoid, mkAbsurd — empty type and ex falso
• mkSum, mkInl, mkInr, mkSumElim — disjoint sum with eliminator
• mkEq, mkRefl, mkJ — identity type with J eliminator

Universes

• mkU : Int → Tm — universe at level i

Axiomatized Primitives (§2.1)

• mkString, mkInt, mkFloat, mkAttrs, mkPath, mkFunction, mkAny — type formers
• mkStringLit, mkIntLit, mkFloatLit, mkAttrsLit, mkPathLit, mkFnLit, mkAnyLit — literal values