Deploying to gh-pages from @ f5c2bb5 🚀

Beluga-lang · Sep 18, 2024 · b02f8ab · b02f8ab
1 parent a9c0a08
commit b02f8ab
Show file tree

Hide file tree

Showing 8 changed files with 79 additions and 144 deletions.
diff --git a/Mcltt.Core.Semantic.PER.Definitions.html b/Mcltt.Core.Semantic.PER.Definitions.html
@@ -57,7 +57,7 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 </div>
 
 <div class="doc">
-<a id="lab1"></a><h2 class="section">Helper Bundles</h2>
+<a id="lab1"></a><h3 class="section">Helper Bundles</h3>
  Related modulo evaluation 
 </div>
 <div class="code">
@@ -84,7 +84,7 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 </div>
 
 <div class="doc">
-<a id="lab2"></a><h2 class="section">(Some Elements of) PER Lattice</h2>
+<a id="lab2"></a><h3 class="section">(Some Elements of) PER Lattice</h3>
 
 </div>
 <div class="code">
@@ -142,7 +142,8 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 </div>
 
 <div class="doc">
-<a id="lab3"></a><h2 class="section">Universe/Element PER Definition</h2>
+<a id="lab3"></a><h1 class="section">Universe/Element PER</h1>
+<a id="lab4"></a><h2 class="section">Universe/Element PER Definition</h2>
 
 </div>
 <div class="code">
@@ -261,7 +262,7 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 </div>
 
 <div class="doc">
-<a id="lab4"></a><h2 class="section">Universe/Element PER Induction Principle</h2>
+<a id="lab5"></a><h2 class="section">Universe/Element PER Induction Principle</h2>
 
 </div>
 <div class="code">
@@ -319,6 +320,15 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 <br/>
 <span class="id" title="keyword">Reserved Notation</span> &quot;'Sub' a &lt;: b 'at' i" (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">judg</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90, <span class="id" title="var">a</span> <span class="id" title="var">custom</span> <span class="id" title="var">domain</span>, <span class="id" title="var">b</span> <span class="id" title="var">custom</span> <span class="id" title="var">domain</span>, <span class="id" title="var">i</span> <span class="id" title="keyword">constr</span>).<br/>
 
+<br/>
+</div>
+
+<div class="doc">
+<a id="lab6"></a><h1 class="section">Universe Subtyping</h1>
+
+</div>
+<div class="code">
+
 <br/>
 <span class="id" title="keyword">Inductive</span> <a id="per_subtyp" class="idref" href="#per_subtyp"><span class="id" title="definition, inductive"><span id="per_subtyp_ind" class="id"><span id="per_subtyp_sind" class="id">per_subtyp</span></span></span></a> : <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#domain"><span class="id" title="inductive">domain</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#domain"><span class="id" title="inductive">domain</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
 | <a id="per_subtyp_neut" class="idref" href="#per_subtyp_neut"><span class="id" title="constructor">per_subtyp_neut</span></a> :<br/>
@@ -347,15 +357,6 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 #[<span class="id" title="var">export</span>]<br/>
 &nbsp;<span class="id" title="keyword">Hint</span> <span class="id" title="keyword">Constructors</span> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#per_subtyp"><span class="id" title="inductive">per_subtyp</span></a> : <span class="id" title="var">mcltt</span>.<br/>
 
-<br/>
-</div>
-
-<div class="doc">
-<a id="lab5"></a><h2 class="section">Context/Environment PER</h2>
-
-</div>
-<div class="code">
-
 <br/>
 <span class="id" title="keyword">Definition</span> <a id="rel_typ" class="idref" href="#rel_typ"><span class="id" title="definition">rel_typ</span></a> <a id="i:733" class="idref" href="#i:733"><span class="id" title="binder">i</span></a> <a id="A:734" class="idref" href="#A:734"><span class="id" title="binder">A</span></a> <a id="cb4b3ec485a1b3943d8b917ebd8a0d3e" class="idref" href="#cb4b3ec485a1b3943d8b917ebd8a0d3e"><span class="id" title="binder">ρ</span></a> <a id="A':736" class="idref" href="#A':736"><span class="id" title="binder">A'</span></a> <a id="48375aae3cd0e421cd716a4fe1341378" class="idref" href="#48375aae3cd0e421cd716a4fe1341378"><span class="id" title="binder">ρ'</span></a> <a id="R':738" class="idref" href="#R':738"><span class="id" title="binder">R'</span></a> := <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#rel_mod_eval"><span class="id" title="inductive">rel_mod_eval</span></a> (<a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#per_univ_elem"><span class="id" title="definition">per_univ_elem</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#i:733"><span class="id" title="variable">i</span></a>) <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#A:734"><span class="id" title="variable">A</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#cb4b3ec485a1b3943d8b917ebd8a0d3e"><span class="id" title="variable">ρ</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#A':736"><span class="id" title="variable">A'</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#48375aae3cd0e421cd716a4fe1341378"><span class="id" title="variable">ρ'</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#R':738"><span class="id" title="variable">R'</span></a>.<br/>
 <span class="id" title="keyword">Arguments</span> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#rel_typ"><span class="id" title="definition">rel_typ</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> /.<br/>
@@ -364,6 +365,15 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 #[<span class="id" title="var">export</span>]<br/>
 <span class="id" title="keyword">Hint</span> <span class="id" title="keyword">Unfold</span> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#rel_typ"><span class="id" title="definition">rel_typ</span></a> : <span class="id" title="var">mcltt</span>.<br/>
 
+<br/>
+</div>
+
+<div class="doc">
+<a id="lab7"></a><h1 class="section">Context/Environment PER</h1>
+
+</div>
+<div class="code">
+
 <br/>
 <span class="id" title="keyword">Inductive</span> <a id="per_ctx_env" class="idref" href="#per_ctx_env"><span class="id" title="definition, inductive"><span id="per_ctx_env_ind" class="id"><span id="per_ctx_env_sind" class="id">per_ctx_env</span></span></span></a> : <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Relations.Relation_Definitions.html#relation"><span class="id" title="definition">relation</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#:::'env'"><span class="id" title="notation">env</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ctx"><span class="id" title="abbreviation">ctx</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ctx"><span class="id" title="abbreviation">ctx</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
 | <a id="per_ctx_env_nil" class="idref" href="#per_ctx_env_nil"><span class="id" title="constructor">per_ctx_env_nil</span></a> :<br/>
@@ -397,6 +407,15 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 <br/>
 <span class="id" title="keyword">Reserved Notation</span> &quot;'SubE' Γ &lt;: Δ" (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">judg</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90, <span class="id" title="var">Γ</span> <span class="id" title="var">custom</span> <span class="id" title="var">exp</span>, <span class="id" title="var">Δ</span> <span class="id" title="var">custom</span> <span class="id" title="var">exp</span>).<br/>
 
+<br/>
+</div>
+
+<div class="doc">
+<a id="lab8"></a><h1 class="section">Context Subtyping</h1>
+
+</div>
+<div class="code">
+
 <br/>
 <span class="id" title="keyword">Inductive</span> <a id="per_ctx_subtyp" class="idref" href="#per_ctx_subtyp"><span class="id" title="definition, inductive"><span id="per_ctx_subtyp_ind" class="id"><span id="per_ctx_subtyp_sind" class="id">per_ctx_subtyp</span></span></span></a> : <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ctx"><span class="id" title="abbreviation">ctx</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ctx"><span class="id" title="abbreviation">ctx</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
 | <a id="per_ctx_subtyp_nil" class="idref" href="#per_ctx_subtyp_nil"><span class="id" title="constructor">per_ctx_subtyp_nil</span></a> :<br/>

diff --git a/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html b/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html
@@ -495,7 +495,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.CoreLemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab6"></a><h2 class="section">Simple Morphism instance for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_univ_elem"><span class="id" title="definition">glu_univ_elem</span></a></span></h2>
+<a id="lab9"></a><h3 class="section">Simple Morphism instance for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_univ_elem"><span class="id" title="definition">glu_univ_elem</span></a></span></h3>
 
 </div>
 <div class="code">
@@ -512,7 +512,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.CoreLemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab7"></a><h2 class="section">Morphism instances for <span class="inlinecode"><span class="id" title="var">neut_glu_</span>*<span class="id" title="var">_pred</span></span>s</h2>
+<a id="lab10"></a><h3 class="section">Morphism instances for <span class="inlinecode"><span class="id" title="var">neut_glu_</span>*<span class="id" title="var">_pred</span></span>s</h3>
 
 </div>
 <div class="code">
@@ -552,7 +552,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.CoreLemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab8"></a><h2 class="section">Morphism instances for <span class="inlinecode"><span class="id" title="var">pi_glu_</span>*<span class="id" title="var">_pred</span></span>s</h2>
+<a id="lab11"></a><h3 class="section">Morphism instances for <span class="inlinecode"><span class="id" title="var">pi_glu_</span>*<span class="id" title="var">_pred</span></span>s</h3>
 
 </div>
 <div class="code">
@@ -782,7 +782,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.CoreLemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab9"></a><h2 class="section">Morphism instances for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_univ_elem"><span class="id" title="definition">glu_univ_elem</span></a></span></h2>
+<a id="lab12"></a><h3 class="section">Morphism instances for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_univ_elem"><span class="id" title="definition">glu_univ_elem</span></a></span></h3>
 
 </div>
 <div class="code">
@@ -1094,7 +1094,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.CoreLemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab10"></a><h2 class="section">Simple Morphism instance for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_ctx_env"><span class="id" title="inductive">glu_ctx_env</span></a></span></h2>
+<a id="lab13"></a><h3 class="section">Simple Morphism instance for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_ctx_env"><span class="id" title="inductive">glu_ctx_env</span></a></span></h3>
 
 </div>
 <div class="code">

diff --git a/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html b/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html
@@ -633,7 +633,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab11"></a><h2 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_typ_with_sub"><span class="id" title="inductive">glu_rel_typ_with_sub</span></a></span> and <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_exp_with_sub"><span class="id" title="inductive">glu_rel_exp_with_sub</span></a></span></h2>
+<a id="lab14"></a><h3 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_typ_with_sub"><span class="id" title="inductive">glu_rel_typ_with_sub</span></a></span> and <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_exp_with_sub"><span class="id" title="inductive">glu_rel_exp_with_sub</span></a></span></h3>
 
 </div>
 <div class="code">
@@ -761,7 +761,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab12"></a><h2 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_ctx_env"><span class="id" title="inductive">glu_ctx_env</span></a></span></h2>
+<a id="lab15"></a><h3 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_ctx_env"><span class="id" title="inductive">glu_ctx_env</span></a></span></h3>
 
 </div>
 <div class="code">
@@ -1167,7 +1167,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab13"></a><h2 class="section">Tactics for <span class="inlinecode"><span class="id" title="var">glu_rel_</span>*</span></h2>
+<a id="lab16"></a><h3 class="section">Tactics for <span class="inlinecode"><span class="id" title="var">glu_rel_</span>*</span></h3>
 
 </div>
 <div class="code">
@@ -1215,7 +1215,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab14"></a><h2 class="section">Lemmas about <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_exp"><span class="id" title="definition">glu_rel_exp</span></a></span></h2>
+<a id="lab17"></a><h3 class="section">Lemmas about <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_exp"><span class="id" title="definition">glu_rel_exp</span></a></span></h3>
 
 </div>
 <div class="code">
@@ -1297,7 +1297,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab15"></a><h2 class="section">Lemmas about <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_sub"><span class="id" title="definition">glu_rel_sub</span></a></span></h2>
+<a id="lab18"></a><h3 class="section">Lemmas about <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_sub"><span class="id" title="definition">glu_rel_sub</span></a></span></h3>
 
 </div>
 <div class="code">

diff --git a/Mcltt.Core.Syntactic.Syntax.html b/Mcltt.Core.Syntactic.Syntax.html
@@ -37,7 +37,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.Syntax</h1>
 </div>
 
 <div class="doc">
-<a id="lab16"></a><h2 class="section">Concrete Syntax Tree</h2>
+<a id="lab19"></a><h1 class="section">Concrete Syntax Tree</h1>
 
 </div>
 <div class="code">
@@ -58,7 +58,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.Syntax</h1>
 </div>
 
 <div class="doc">
-<a id="lab17"></a><h2 class="section">Abstract Syntac Tree</h2>
+<a id="lab20"></a><h1 class="section">Abstract Syntac Tree</h1>
 
 </div>
 <div class="code">
@@ -142,7 +142,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.Syntax</h1>
 </div>
 
 <div class="doc">
-<a id="lab18"></a><h3 class="section">Syntactic Normal/Neutral Form</h3>
+<a id="lab21"></a><h2 class="section">Syntactic Normal/Neutral Form</h2>
 
 </div>
 <div class="code">
@@ -209,6 +209,13 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.Syntax</h1>
 <span class="id" title="keyword">Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">mcltt_scope</span>.<br/>
 
 <br/>
+</div>
+
+<div class="doc">
+<a id="lab22"></a><h2 class="section">Syntactic Notations</h2>
+
+</div>
+<div class="code">
 <span class="id" title="keyword">Module</span> <a id="Syntax_Notations" class="idref" href="#Syntax_Notations"><span class="id" title="module">Syntax_Notations</span></a>.<br/>
 &nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a id="ff90a81e6f1b3c561f471442d9455cb9" class="idref" href="#ff90a81e6f1b3c561f471442d9455cb9"><span class="id" title="notation">&quot;</span></a>{{{ x }}}" := <span class="id" title="var">x</span> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">exp</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99, <span class="id" title="var">format</span> "'{{{'  x  '}}}'") : <span class="id" title="var">mcltt_scope</span>.<br/>
 &nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a id="b8b673de4d770a3cbcbccee376638293" class="idref" href="#b8b673de4d770a3cbcbccee376638293"><span class="id" title="notation">&quot;</span></a>( x )" := <span class="id" title="var">x</span> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">exp</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">exp</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60) : <span class="id" title="var">mcltt_scope</span>.<br/>