# theoria v0.1.0 - Table of Contents

> An Elixir-native proof/spec kernel inspired by trusted theorem prover kernels.

## Pages

- [Theoria](readme.md)
- [Theoria Design](design.md)
- [LICENSE](license.md)

## Modules

- [Theoria](Theoria.md): An Elixir-native proof/spec kernel inspired by Lean's trusted-kernel design.
- [Theoria.Context](Theoria.Context.md): Typing context for bound variables.
- [Theoria.Env](Theoria.Env.md): Kernel environment containing checked constants and definitions.

- [Theoria.Env.Constant](Theoria.Env.Constant.md): A checked constant or definition in a kernel environment.
- [Theoria.Kernel](Theoria.Kernel.md): The trusted type-checking kernel.
- [Theoria.Normalize](Theoria.Normalize.md): Normalization and definitional equality for core terms.
- [Theoria.Term](Theoria.Term.md): Core terms for Theoria's trusted kernel.
- [Theoria.Term.App](Theoria.Term.App.md): Function application.
- [Theoria.Term.BVar](Theoria.Term.BVar.md): A bound variable represented by a de Bruijn index.
- [Theoria.Term.Const](Theoria.Term.Const.md): A named environment constant.
- [Theoria.Term.Forall](Theoria.Term.Forall.md): Dependent function type. Non-dependent functions are encoded as forall types.
- [Theoria.Term.Lam](Theoria.Term.Lam.md): Lambda abstraction.
- [Theoria.Term.Sort](Theoria.Term.Sort.md): A universe level, written `Type n` in the surface language.

- Exceptions
  - [Theoria.Error](Theoria.Error.md): Kernel error returned when a term cannot be checked.