Type Checker

Semi-trusted (Layer 1): uses the TCB (eval/quote/conv) and reports type errors via send "typeError". Bugs...

Checks whether two values are definitionally equal at a given binding depth. Purely structural — no type information...

Bridges the fx.types layer to the kernel's term representation via the HOAS combinator layer. Provides the Nix ↔ kernel...

Pure evaluator: interprets kernel terms in an environment of values. Zero effect system imports — part of the trusted...

Higher-Order Abstract Syntax layer that lets you write kernel terms using Nix lambdas for variable binding. The...

Converts values back to terms, translating de Bruijn levels to indices. Pure function — part of the TCB. Spec...

Syntax of the kernel's term language. All 48 constructors produce attrsets with a tag field (not _tag, to distinguish...

Values are the semantic domain produced by evaluation. They use de Bruijn levels (counting outward from the top of the...

High-level combinators for writing kernel-checked implementations. Write programs with these combinators, then call...