Deploying to gh-pages from @ 44c8633 🚀

Beluga-lang · Oct 4, 2024 · c570bc0 · c570bc0
1 parent 886e9c9
commit c570bc0
Show file tree

Hide file tree

Showing 8 changed files with 2,449 additions and 2,126 deletions.
diff --git a/ext/prop-eq/Mcltt.Core.Syntactic.CtxSub.html b/ext/prop-eq/Mcltt.Core.Syntactic.CtxSub.html
diff --git a/ext/prop-eq/Mcltt.Core.Syntactic.Presup.html b/ext/prop-eq/Mcltt.Core.Syntactic.Presup.html
diff --git a/ext/prop-eq/Mcltt.Core.Syntactic.Syntax.html b/ext/prop-eq/Mcltt.Core.Syntactic.Syntax.html
@@ -289,7 +289,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.Syntax</h1>
 
 <br/>
 &nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a id="9b92ee7199d69b3fa5fcca8194180e8f" class="idref" href="#9b92ee7199d69b3fa5fcca8194180e8f"><span class="id" title="notation">&quot;</span></a>⋅" := <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Datatypes.html#nil"><span class="id" title="constructor">nil</span></a> (<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">mcltt_scope</span>.<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a id="d1064cbf3bcb4d3b63e8559a3ab3b23c" class="idref" href="#d1064cbf3bcb4d3b63e8559a3ab3b23c"><span class="id" title="notation">&quot;</span></a>x , y" := (<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Datatypes.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">y</span> <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> 50, <span class="id" title="var">format</span> "x ,  y") : <span class="id" title="var">mcltt_scope</span>.<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a id="d1064cbf3bcb4d3b63e8559a3ab3b23c" class="idref" href="#d1064cbf3bcb4d3b63e8559a3ab3b23c"><span class="id" title="notation">&quot;</span></a>x , y" := (<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Datatypes.html#cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">y</span> <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> 50, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">format</span> "x ,  y") : <span class="id" title="var">mcltt_scope</span>.<br/>
 
 <br/>
 &nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a id="145dc3c72ee505d62ea64134c16fa77a" class="idref" href="#145dc3c72ee505d62ea64134c16fa77a"><span class="id" title="notation">&quot;</span></a>n{{{ 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">nf</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99, <span class="id" title="var">format</span> "'n{{{'  x  '}}}'") : <span class="id" title="var">mcltt_scope</span>.<br/>

diff --git a/ext/prop-eq/Mcltt.Core.Syntactic.System.Definitions.html b/ext/prop-eq/Mcltt.Core.Syntactic.System.Definitions.html
diff --git a/ext/prop-eq/Mcltt.Core.Syntactic.System.Lemmas.html b/ext/prop-eq/Mcltt.Core.Syntactic.System.Lemmas.html
diff --git a/ext/prop-eq/Mcltt.LibTactics.html b/ext/prop-eq/Mcltt.LibTactics.html
@@ -51,7 +51,7 @@ <h1 class="libtitle">Mcltt.LibTactics</h1>
 </div>
 
 <div class="doc">
-<a id="lab15"></a><h3 class="section">Generalization of Variables</h3>
+<a id="lab16"></a><h3 class="section">Generalization of Variables</h3>
 
 </div>
 <div class="code">
@@ -66,7 +66,7 @@ <h1 class="libtitle">Mcltt.LibTactics</h1>
 </div>
 
 <div class="doc">
-<a id="lab16"></a><h3 class="section">Marking-based Tactics</h3>
+<a id="lab17"></a><h3 class="section">Marking-based Tactics</h3>
 
 </div>
 <div class="code">
@@ -121,7 +121,7 @@ <h1 class="libtitle">Mcltt.LibTactics</h1>
 </div>
 
 <div class="doc">
-<a id="lab17"></a><h3 class="section">Simple helper</h3>
+<a id="lab18"></a><h3 class="section">Simple helper</h3>
 
 </div>
 <div class="code">
@@ -281,7 +281,7 @@ <h1 class="libtitle">Mcltt.LibTactics</h1>
 </div>
 
 <div class="doc">
-<a id="lab18"></a><h3 class="section">McLTT automation</h3>
+<a id="lab19"></a><h3 class="section">McLTT automation</h3>
 
 </div>
 <div class="code">
@@ -555,7 +555,7 @@ <h1 class="libtitle">Mcltt.LibTactics</h1>
 </div>
 
 <div class="doc">
-<a id="lab19"></a><h3 class="section">Helper Instances for Generalized Rewriting</h3>
+<a id="lab20"></a><h3 class="section">Helper Instances for Generalized Rewriting</h3>
 
 </div>
 <div class="code">

diff --git a/ext/prop-eq/indexpage.html b/ext/prop-eq/indexpage.html
diff --git a/ext/prop-eq/toc.html b/ext/prop-eq/toc.html
@@ -55,7 +55,10 @@ <h2><a href="Mcltt.Core.Syntactic.System.Definitions.html">Mcltt.Core.Syntactic.
 <h2><a href="Mcltt.Core.Syntactic.System.Lemmas.html">Mcltt.Core.Syntactic.System.Lemmas</a></h2>
 <ul class="doclist">
 <li><ul class="doclist">
-<li><a href="Mcltt.Core.Syntactic.System.Lemmas.html#lab5">Core Presuppositions</a>
+<li><a href="Mcltt.Core.Syntactic.System.Lemmas.html#lab5">Basic Context Properties</a>
+
+</li>
+<li><a href="Mcltt.Core.Syntactic.System.Lemmas.html#lab6">Core Presuppositions</a>
 
 </li>
 </ul>