Skip to content

Commit

Permalink
Deploying to gh-pages from @ 2e24420 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@MartyO256
MartyO256 committed Dec 5, 2023
1 parent 6f33dd2 commit 7d70b01
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion beluga/Synext/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@
});

//]]>
</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">beluga</a> &#x00BB; Synext</nav><header class="odoc-preamble"><h1>Module <code><span>Synext</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#external-syntax-definition">External Syntax Definition</a><ul><li><a href="#external-lf-syntax">External LF Syntax</a></li><li><a href="#external-contextual-lf-syntax">External Contextual LF Syntax</a></li><li><a href="#external-meta-syntax">External Meta-Syntax</a></li><li><a href="#external-computation-level-syntax">External Computation-Level Syntax</a></li><li><a href="#external-harpoon-syntax">External Harpoon Syntax</a></li><li><a href="#external-signature-syntax">External Signature Syntax</a></li><li><a href="#constants">Constants</a></li><li><a href="#type-aliases">Type Aliases</a><ul><li><a href="#lf">LF</a></li><li><a href="#contextual-lf">Contextual LF</a></li><li><a href="#meta-level">Meta-level</a></li><li><a href="#computation-level">Computation-level</a></li><li><a href="#harpoon">Harpoon</a></li><li><a href="#signature">Signature</a></li></ul></li></ul></li><li><a href="#common">Common</a></li><li><a href="#locations">Locations</a><ul><li><a href="#lf_2">LF</a></li><li><a href="#contextual-lf_2">Contextual LF</a></li><li><a href="#meta-level_2">Meta-Level</a></li><li><a href="#computation-level_2">Computation-Level</a></li><li><a href="#harpoon_2">Harpoon</a></li><li><a href="#signature_2">Signature</a></li></ul></li><li><a href="#precedences">Precedences</a></li><li><a href="#explicit-arguments">Explicit Arguments</a></li><li><a href="#pretty-printing_2">Pretty-Printing</a></li></ul></nav><div class="odoc-content"><h2 id="external-syntax-definition"><a href="#external-syntax-definition" class="anchor"></a>External Syntax Definition</h2><p>ASTs constructed with the constructors in this module are not necessarily in normal form.</p><p>These types are suited for pretty-printing and elaboration to the internal syntax. Note that this is a named representation without ambiguities.</p><p>There are three kinds of variables to consider in Beluga:</p><ul><li>LF-bound variables, which are introduced by LF abstractions and contexts, and range over pure LF terms (not contextual LF terms).</li><li>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.</li><li>Computation-level variables, which are introduced by computation-level patterns, and range over computation-level expressions.</li></ul><p>Contextual variables are further classified in four variants:</p><ul><li>Meta-variables, which range over contextual LF terms.</li><li>Context variables, which range over contextual LF contexts.</li><li>Parameter variables, prefixed by <code>#</code>, which range over contextual LF terms. These are bound variables implicit to a context variable.</li><li>Substitution variables, prefixed by <code>$</code>, which range over contextual LF substitutions.</li></ul><h3 id="external-lf-syntax"><a href="#external-lf-syntax" class="anchor"></a>External LF Syntax</h3><p>The representation of LF kinds, types, and terms after parsing and data-dependent disambiguation.</p><p>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.</p><p>LF terms as defined below may contain free variables. During the abstraction phase of term reconstruction, implicit binders are introduced for those free variables.</p><p>In the following grammar, the metavariable:</p><ul><li><code class="odoc-katex-math">x</code> ranges over variables</li><li><code class="odoc-katex-math">c</code> ranges over term-level constants</li><li><code class="odoc-katex-math">a</code> ranges over type-level constants</li></ul><div><pre class="odoc-katex-math display"> \begin{aligned}
</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">beluga</a> &#x00BB; Synext</nav><header class="odoc-preamble"><h1>Module <code><span>Synext</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#external-syntax-definition">External Syntax Definition</a><ul><li><a href="#external-lf-syntax">External LF Syntax</a></li><li><a href="#external-contextual-lf-syntax">External Contextual LF Syntax</a></li><li><a href="#external-meta-syntax">External Meta-Syntax</a></li><li><a href="#external-computation-level-syntax">External Computation-Level Syntax</a></li><li><a href="#external-harpoon-syntax">External Harpoon Syntax</a></li><li><a href="#external-signature-syntax">External Signature Syntax</a></li><li><a href="#constants">Constants</a></li><li><a href="#type-aliases">Type Aliases</a><ul><li><a href="#lf">LF</a></li><li><a href="#contextual-lf">Contextual LF</a></li><li><a href="#meta-level">Meta-level</a></li><li><a href="#computation-level">Computation-level</a></li><li><a href="#harpoon">Harpoon</a></li><li><a href="#signature">Signature</a></li></ul></li></ul></li><li><a href="#common">Common</a></li><li><a href="#locations">Locations</a><ul><li><a href="#lf_2">LF</a></li><li><a href="#contextual-lf_2">Contextual LF</a></li><li><a href="#meta-level_2">Meta-Level</a></li><li><a href="#computation-level_2">Computation-Level</a></li><li><a href="#harpoon_2">Harpoon</a></li><li><a href="#signature_2">Signature</a></li></ul></li><li><a href="#precedences">Precedences</a></li><li><a href="#explicit-arguments">Explicit Arguments</a></li><li><a href="#pretty-printing_2">Pretty-Printing</a></li></ul></nav><div class="odoc-content"><h2 id="external-syntax-definition"><a href="#external-syntax-definition" class="anchor"></a>External Syntax Definition</h2><p>ASTs constructed with the constructors in this module are not necessarily in normal form.</p><p>These types are suited for pretty-printing and elaboration to the internal syntax. Note that this is a named representation without ambiguities.</p><p>There are three kinds of variables to consider in Beluga:</p><ul><li>LF-bound variables, which are introduced by LF abstractions and contexts, and range over pure LF terms (not contextual LF terms).</li><li>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.</li><li>Computation-level variables, which are introduced by computation-level patterns, and range over computation-level expressions.</li></ul><p>Contextual variables are further classified in four variants:</p><ul><li>Meta-variables, which range over contextual LF terms.</li><li>Context variables, which range over contextual LF contexts.</li><li>Parameter variables, prefixed by <code>#</code>, which range over contextual LF terms. These are bound variables implicit to a context variable.</li><li>Substitution variables, prefixed by <code>$</code>, which range over contextual LF substitutions.</li></ul><h3 id="external-lf-syntax"><a href="#external-lf-syntax" class="anchor"></a>External LF Syntax</h3><p>The representation of LF kinds, types, and terms after parsing and data-dependent disambiguation.</p><p>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.</p><p>LF terms as defined below may contain free variables. During the abstraction phase of term reconstruction, implicit binders are introduced for those free variables.</p><p>In the following grammar, the metavariable:</p><ul><li><code class="odoc-katex-math">x</code> ranges over variables</li><li><code class="odoc-katex-math">c</code> ranges over term-level constants</li><li><code class="odoc-katex-math">a</code> ranges over type-level constants</li></ul><div><pre class="odoc-katex-math display"> \begin{aligned}
&amp;\text{LF kinds} &amp;K &amp;\Coloneqq
\mathsf{type}
\mid \Pi x {:} A. K
Expand Down

0 comments on commit 7d70b01

Please sign in to comment.