Modules
An Elixir-native proof/spec kernel inspired by Lean's trusted-kernel design.
Typing context for bound variables.
Kernel environment containing checked constants and definitions.
A checked constant or definition in a kernel environment.
Kernel error returned when a term cannot be checked.
The trusted type-checking kernel.
Normalization and definitional equality for core terms.
Core terms for Theoria's trusted kernel.
Function application.
A bound variable represented by a de Bruijn index.
A named environment constant.
Dependent function type. Non-dependent functions are encoded as forall types.
Lambda abstraction.
A universe level, written Type n in the surface language.