deploy: cae160f

hferee · Sep 3, 2024 · 62e9fa7 · 62e9fa7
commit 62e9fa7
Show file tree

Hide file tree

Showing 106 changed files with 86,421 additions and 0 deletions.
diff --git a/GL.GLS.DLW_wf_lex.html b/GL.GLS.DLW_wf_lex.html
diff --git a/GL.GLS.GLS_additive_cut.html b/GL.GLS.GLS_additive_cut.html
diff --git a/GL.GLS.GLS_calcs.html b/GL.GLS.GLS_calcs.html
diff --git a/GL.GLS.GLS_ctr.html b/GL.GLS.GLS_ctr.html
diff --git a/GL.GLS.GLS_cut_elim.html b/GL.GLS.GLS_cut_elim.html
diff --git a/GL.GLS.GLS_dec.html b/GL.GLS.GLS_dec.html
diff --git a/GL.GLS.GLS_der_dec.html b/GL.GLS.GLS_der_dec.html
diff --git a/GL.GLS.GLS_exch.html b/GL.GLS.GLS_exch.html
diff --git a/GL.GLS.GLS_export.html b/GL.GLS.GLS_export.html
@@ -0,0 +1,51 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
+<script type="text/javascript" src="config.js"></script>
+<script type="text/javascript" src="coqdocjs.js"></script>
+</head>
+
+<body onload="document.getElementById('content').focus()">
+  <div id="header">
+    <span class="left">
+      <span class="modulename"> <script> document.write(document.title) </script> </span>
+    </span>
+
+    <span class="button" id="toggle-proofs"></span>
+
+    <span class="right">
+      <a href="https://github.com/hferee/UIML">Project Page</a>
+      <a href="./indexpage.html"> Index </a>
+      <a href="./toc.html"> Table of Contents </a>
+      <a href="./demo.html"> Demo </a>
+    </span>
+</div>
+    <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
+    <div id="main">
+<h1 class="libtitle">GL.GLS.GLS_export</h1>
+
+<div class="code">
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="GL.GLS.GLS_calcs.html#"><span class="id" title="library">GLS_calcs</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="GL.GLS.GLS_dec.html#"><span class="id" title="library">GLS_dec</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="GL.GLS.GLS_exch.html#"><span class="id" title="library">GLS_exch</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="GL.GLS.GLS_ctr.html#"><span class="id" title="library">GLS_ctr</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="GL.GLS.GLS_wkn.html#"><span class="id" title="library">GLS_wkn</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="GL.GLS.GLS_inv_ImpR_ImpL.html#"><span class="id" title="library">GLS_inv_ImpR_ImpL</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="GL.GLS.DLW_wf_lex.html#"><span class="id" title="library">DLW_wf_lex</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="GL.GLS.GLS_termination_measure.html#"><span class="id" title="library">GLS_termination_measure</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="GL.GLS.GLS_der_dec.html#"><span class="id" title="library">GLS_der_dec</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="GL.GLS.GLS_additive_cut.html#"><span class="id" title="library">GLS_additive_cut</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="GL.GLS.GLS_cut_elim.html#"><span class="id" title="library">GLS_cut_elim</span></a>.<br/>
+</div>
+</div>
+<div id="footer">
+  Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
+</div>
+</div>
+</body>
+
+</html>
diff --git a/GL.GLS.GLS_inv_ImpR_ImpL.html b/GL.GLS.GLS_inv_ImpR_ImpL.html
diff --git a/GL.GLS.GLS_termination_measure.html b/GL.GLS.GLS_termination_measure.html
diff --git a/GL.GLS.GLS_wkn.html b/GL.GLS.GLS_wkn.html
diff --git a/GL.Interpolation.UIGL_And_Or_rules.html b/GL.Interpolation.UIGL_And_Or_rules.html
diff --git a/GL.Interpolation.UIGL_Canopy.html b/GL.Interpolation.UIGL_Canopy.html
diff --git a/GL.Interpolation.UIGL_Canopy_ImpL.html b/GL.Interpolation.UIGL_Canopy_ImpL.html
diff --git a/GL.Interpolation.UIGL_Canopy_ImpR.html b/GL.Interpolation.UIGL_Canopy_ImpR.html
diff --git a/GL.Interpolation.UIGL_Canopy_nodupseq_perm.html b/GL.Interpolation.UIGL_Canopy_nodupseq_perm.html
diff --git a/GL.Interpolation.UIGL_Def_measure.html b/GL.Interpolation.UIGL_Def_measure.html
diff --git a/GL.Interpolation.UIGL_Diam_N_imp_UI.html b/GL.Interpolation.UIGL_Diam_N_imp_UI.html
diff --git a/GL.Interpolation.UIGL_Diam_UI_imp_N.html b/GL.Interpolation.UIGL_Diam_UI_imp_N.html
diff --git a/GL.Interpolation.UIGL_Diam_UI_imp_N_prelim.html b/GL.Interpolation.UIGL_Diam_UI_imp_N_prelim.html
diff --git a/GL.Interpolation.UIGL_LexSeq.html b/GL.Interpolation.UIGL_LexSeq.html
diff --git a/GL.Interpolation.UIGL_N_imp_UI.html b/GL.Interpolation.UIGL_N_imp_UI.html
diff --git a/GL.Interpolation.UIGL_PermutationT.html b/GL.Interpolation.UIGL_PermutationT.html
diff --git a/GL.Interpolation.UIGL_PermutationTS.html b/GL.Interpolation.UIGL_PermutationTS.html
diff --git a/GL.Interpolation.UIGL_UIDiam_N.html b/GL.Interpolation.UIGL_UIDiam_N.html
diff --git a/GL.Interpolation.UIGL_UIOne.html b/GL.Interpolation.UIGL_UIOne.html
diff --git a/GL.Interpolation.UIGL_UIThree.html b/GL.Interpolation.UIGL_UIThree.html
diff --git a/GL.Interpolation.UIGL_UITwo.html b/GL.Interpolation.UIGL_UITwo.html
diff --git a/GL.Interpolation.UIGL_UI_inter.html b/GL.Interpolation.UIGL_UI_inter.html
diff --git a/GL.Interpolation.UIGL_UI_prelims.html b/GL.Interpolation.UIGL_UI_prelims.html
diff --git a/GL.Interpolation.UIGL_basics.html b/GL.Interpolation.UIGL_basics.html
diff --git a/GL.Interpolation.UIGL_braga.html b/GL.Interpolation.UIGL_braga.html
diff --git a/GL.Interpolation.UIGL_irred_high_level.html b/GL.Interpolation.UIGL_irred_high_level.html
diff --git a/GL.Interpolation.UIGL_irred_short.html b/GL.Interpolation.UIGL_irred_short.html
diff --git a/GL.Interpolation.UIGL_nodupseq.html b/GL.Interpolation.UIGL_nodupseq.html
diff --git a/General.List_lemmasT.html b/General.List_lemmasT.html
diff --git a/General.ddT.html b/General.ddT.html
diff --git a/General.dd_fc.html b/General.dd_fc.html
diff --git a/General.existsT.html b/General.existsT.html
@@ -0,0 +1,50 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
+<script type="text/javascript" src="config.js"></script>
+<script type="text/javascript" src="coqdocjs.js"></script>
+</head>
+
+<body onload="document.getElementById('content').focus()">
+  <div id="header">
+    <span class="left">
+      <span class="modulename"> <script> document.write(document.title) </script> </span>
+    </span>
+
+    <span class="button" id="toggle-proofs"></span>
+
+    <span class="right">
+      <a href="https://github.com/hferee/UIML">Project Page</a>
+      <a href="./indexpage.html"> Index </a>
+      <a href="./toc.html"> Table of Contents </a>
+      <a href="./demo.html"> Demo </a>
+    </span>
+</div>
+    <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
+    <div id="main">
+<h1 class="libtitle">General.existsT</h1>
+
+<div class="code">
+<span class="id" title="keyword">Notation</span> <a id="1c1c78eb8010a689d430e9cce412ba6d" class="idref" href="#1c1c78eb8010a689d430e9cce412ba6d"><span class="id" title="notation">&quot;</span></a>'existsT' x .. y , p" := (<a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Specif.html#sig"><span class="id" title="inductive">sig</span></a> (<span class="id" title="keyword">fun</span> <a id="x:1" class="idref" href="#x:1"><span class="id" title="binder">x</span></a> =&gt; .. (<a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Specif.html#sig"><span class="id" title="inductive">sig</span></a> (<span class="id" title="keyword">fun</span> <a id="y:2" class="idref" href="#y:2"><span class="id" title="binder">y</span></a> =&gt; <span class="id" title="var">p</span>)) ..))<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 200, <span class="id" title="var">x</span> <span class="id" title="var">binder</span>, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>,<br/>
+&nbsp;&nbsp;&nbsp;<span class="id" title="var">format</span> "'[' 'existsT'  '/  ' x  ..  y ,  '/  ' p ']'")<br/>
+&nbsp;&nbsp;: <span class="id" title="var">type_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a id="d5d0a9fc4a816718ae884ae33cb7068b" class="idref" href="#d5d0a9fc4a816718ae884ae33cb7068b"><span class="id" title="notation">&quot;</span></a>'existsT2' x .. y , p" := (<a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Specif.html#sigT"><span class="id" title="inductive">sigT</span></a> (<span class="id" title="keyword">fun</span> <a id="x:3" class="idref" href="#x:3"><span class="id" title="binder">x</span></a> =&gt; .. (<a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Specif.html#sigT"><span class="id" title="inductive">sigT</span></a> (<span class="id" title="keyword">fun</span> <a id="y:4" class="idref" href="#y:4"><span class="id" title="binder">y</span></a> =&gt; <span class="id" title="var">p</span>)) ..))<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 200, <span class="id" title="var">x</span> <span class="id" title="var">binder</span>, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>,<br/>
+&nbsp;&nbsp;&nbsp;<span class="id" title="var">format</span> "'[' 'existsT2'  '/  ' x  ..  y ,  '/  ' p ']'")<br/>
+&nbsp;&nbsp;: <span class="id" title="var">type_scope</span>.<br/>
+</div>
+</div>
+<div id="footer">
+  Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
+</div>
+</div>
+</body>
+
+</html>