SynextASTs constructed with the constructors in this module are not necessarily in normal form.
These types are suited for pretty-printing and elaboration to the internal syntax. Note that this is a named representation without ambiguities.
There are three kinds of variables to consider in Beluga:
Contextual variables are further classified in four variants:
#, which range over contextual LF terms. These are bound variables implicit to a context variable.$, which range over contextual LF substitutions.The representation of LF kinds, types, and terms after parsing and data-dependent disambiguation.
These types are only intended to be used in the definition of LF type-level or term-level constants. Thi The modules are used s is a weak, representational function space without case analysis or recursion.
LF terms as defined below may contain free variables. During the abstraction phase of term reconstruction, implicit binders are introduced for those free variables.
In the following grammar, the metavariable:
x ranges over variablesc ranges over term-level constantsa ranges over type-level constants \begin{aligned}
+Module Synext
External Syntax Definition
ASTs constructed with the constructors in this module are not necessarily in normal form.
These types are suited for pretty-printing and elaboration to the internal syntax. Note that this is a named representation without ambiguities.
There are three kinds of variables to consider in Beluga:
- LF-bound variables, which are introduced by LF abstractions and contexts, and range over pure LF terms (not contextual LF terms).
- Contextual (or meta-level) variables, which are introduced by computation-level Pi types, dependent type abstractions and meta-object patterns, and range over meta-objects.
- Computation-level variables, which are introduced by computation-level patterns, and range over computation-level expressions.
Contextual variables are further classified in four variants:
- Meta-variables, which range over contextual LF terms.
- Context variables, which range over contextual LF contexts.
- Parameter variables, prefixed by
#, which range over contextual LF terms. These are bound variables implicit to a context variable. - Substitution variables, prefixed by
$, which range over contextual LF substitutions.
External LF Syntax
The representation of LF kinds, types, and terms after parsing and data-dependent disambiguation.
These types are only intended to be used in the definition of LF type-level or term-level constants. This is a weak, representational function space without case analysis or recursion.
LF terms as defined below may contain free variables. During the abstraction phase of term reconstruction, implicit binders are introduced for those free variables.
In the following grammar, the metavariable:
x ranges over variablesc ranges over term-level constantsa ranges over type-level constants
\begin{aligned}
&\text{LF kinds} &K &\Coloneqq
\mathsf{type}
\mid \Pi x {:} A. K