Small Elixir DSL for constructing named Theoria syntax terms.
The DSL is deliberately untrusted. It only builds Theoria.Syntax values;
terms must still be elaborated and checked by Theoria.Kernel.
Summary
Functions
Imports the term-construction DSL.
Function application.
Non-dependent function type.
Applies fun to all args left-associatively.
A named environment constant.
The current core proposition universe, for APIs that need a checked core term.
Elaborates a named syntax term to a core term.
Elaborates a named syntax term or raises Theoria.Error.
Propositional equality.
Equality recursor.
Dependent function type with do block syntax.
Lambda abstraction with do block syntax.
The current proposition universe.
Reflexivity proof.
Builds a Theoria syntax term from a small Elixir-like quoted expression.
A type universe. type(0) corresponds to Type 0, whose core sort is Sort 1.
A named bound variable.
Functions
Imports the term-construction DSL.
Function application.
Non-dependent function type.
Applies fun to all args left-associatively.
A named environment constant.
The current core proposition universe, for APIs that need a checked core term.
Elaborates a named syntax term to a core term.
Elaborates a named syntax term or raises Theoria.Error.
Propositional equality.
Equality recursor.
Dependent function type with do block syntax.
Lambda abstraction with do block syntax.
The current proposition universe.
Reflexivity proof.
Builds a Theoria syntax term from a small Elixir-like quoted expression.
A type universe. type(0) corresponds to Type 0, whose core sort is Sort 1.
A named bound variable.