Deploy to GitHub pages

kth-step · Jan 17, 2024 · 65577fa · 65577fa
commit 65577fa
Show file tree

Hide file tree

Showing 11 changed files with 1,930 additions and 0 deletions.
diff --git a/.nojekyll b/.nojekyll
diff --git a/docs/coqdoc/ABS.abs_defs.html b/docs/coqdoc/ABS.abs_defs.html
diff --git a/docs/coqdoc/ABS.abs_functional_metatheory.html b/docs/coqdoc/ABS.abs_functional_metatheory.html
@@ -0,0 +1,74 @@
+<!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="./../..">Project Website</a>
+      <a href="./indexpage.html">Index</a>
+      <a href="./toc.html">Table of Contents</a>
+    </span>
+</div>
+    <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
+    <div id="main">
+<div class="code">
+<span class="id" title="keyword">From</span> <span class="id" title="var">ABS</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ABS.abs_defs.html#"><span class="id" title="library">abs_defs</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Lists.List.html#"><span class="id" title="library">List</span></a>.<br/>
+<span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Lists.List.html#ListNotations"><span class="id" title="module">ListNotations</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+<a id="lab2"></a><h1 class="section">ABS Functional Metatheory</h1>
+
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a id="subG" class="idref" href="#subG"><span class="id" title="definition">subG</span></a> (<a id="G1:1" class="idref" href="#G1:1"><span class="id" title="binder">G1</span></a> <a id="G2:2" class="idref" href="#G2:2"><span class="id" title="binder">G2</span></a> : <a class="idref" href="ABS.abs_defs.html#G"><span class="id" title="definition">G</span></a>) : <span class="id" title="keyword">Prop</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">forall</span> (<a id="key:3" class="idref" href="#key:3"><span class="id" title="binder">key</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<a id="elt:4" class="idref" href="#elt:4"><span class="id" title="binder">elt</span></a> : <a class="idref" href="ABS.abs_defs.html#ctxv"><span class="id" title="inductive">ctxv</span></a>), <br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ABS.abs_defs.html#Map.find"><span class="id" title="definition">Map.find</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#key:3"><span class="id" title="variable">key</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#G1:1"><span class="id" title="variable">G1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#elt:4"><span class="id" title="variable">elt</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ABS.abs_defs.html#Map.find"><span class="id" title="definition">Map.find</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#key:3"><span class="id" title="variable">key</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#G2:2"><span class="id" title="variable">G2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#elt:4"><span class="id" title="variable">elt</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a id="G_vdash_s" class="idref" href="#G_vdash_s"><span class="id" title="definition">G_vdash_s</span></a> (<a id="G5:5" class="idref" href="#G5:5"><span class="id" title="binder">G5</span></a> : <a class="idref" href="ABS.abs_defs.html#G"><span class="id" title="definition">G</span></a>) (<a id="s5:6" class="idref" href="#s5:6"><span class="id" title="binder">s5</span></a> : <a class="idref" href="ABS.abs_defs.html#s"><span class="id" title="definition">s</span></a>) :=<br/>
+&nbsp;<span class="id" title="keyword">forall</span> (<a id="x5:7" class="idref" href="#x5:7"><span class="id" title="binder">x5</span></a> : <a class="idref" href="ABS.abs_defs.html#x"><span class="id" title="definition">x</span></a>) (<a id="t5:8" class="idref" href="#t5:8"><span class="id" title="binder">t5</span></a> : <a class="idref" href="ABS.abs_defs.html#t"><span class="id" title="inductive">t</span></a>) (<a id="T5:9" class="idref" href="#T5:9"><span class="id" title="binder">T5</span></a> : <a class="idref" href="ABS.abs_defs.html#T"><span class="id" title="inductive">T</span></a>),<br/>
+&nbsp;&nbsp;<a class="idref" href="ABS.abs_defs.html#Map.find"><span class="id" title="definition">Map.find</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#x5:7"><span class="id" title="variable">x5</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#s5:6"><span class="id" title="variable">s5</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#t5:8"><span class="id" title="variable">t5</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="ABS.abs_defs.html#Map.find"><span class="id" title="definition">Map.find</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#x5:7"><span class="id" title="variable">x5</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#G5:5"><span class="id" title="variable">G5</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> (<a class="idref" href="ABS.abs_defs.html#ctxv_T"><span class="id" title="constructor">ctxv_T</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#T5:9"><span class="id" title="variable">T5</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="ABS.abs_defs.html#typ_e"><span class="id" title="inductive">typ_e</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#G5:5"><span class="id" title="variable">G5</span></a> (<a class="idref" href="ABS.abs_defs.html#e_t"><span class="id" title="constructor">e_t</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#t5:8"><span class="id" title="variable">t5</span></a>) <a class="idref" href="ABS.abs_functional_metatheory.html#T5:9"><span class="id" title="variable">T5</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a id="type_preservation" class="idref" href="#type_preservation"><span class="id" title="lemma">type_preservation</span></a> : <span class="id" title="keyword">forall</span> (<a id="G5:10" class="idref" href="#G5:10"><span class="id" title="binder">G5</span></a> : <a class="idref" href="ABS.abs_defs.html#G"><span class="id" title="definition">G</span></a>) (<a id="s5:11" class="idref" href="#s5:11"><span class="id" title="binder">s5</span></a> : <a class="idref" href="ABS.abs_defs.html#s"><span class="id" title="definition">s</span></a>), <br/>
+&nbsp;&nbsp;<a class="idref" href="ABS.abs_functional_metatheory.html#G_vdash_s"><span class="id" title="definition">G_vdash_s</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#G5:10"><span class="id" title="variable">G5</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#s5:11"><span class="id" title="variable">s5</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">forall</span> (<a id="Flist:12" class="idref" href="#Flist:12"><span class="id" title="binder">Flist</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ABS.abs_defs.html#F"><span class="id" title="inductive">F</span></a>) (<a id="e5:13" class="idref" href="#e5:13"><span class="id" title="binder">e5</span></a> : <a class="idref" href="ABS.abs_defs.html#e"><span class="id" title="inductive">e</span></a>) (<a id="T5:14" class="idref" href="#T5:14"><span class="id" title="binder">T5</span></a> : <a class="idref" href="ABS.abs_defs.html#T"><span class="id" title="inductive">T</span></a>) (<a id="s':15" class="idref" href="#s':15"><span class="id" title="binder">s'</span></a> : <a class="idref" href="ABS.abs_defs.html#s"><span class="id" title="definition">s</span></a>) (<a id="e':16" class="idref" href="#e':16"><span class="id" title="binder">e'</span></a> : <a class="idref" href="ABS.abs_defs.html#e"><span class="id" title="inductive">e</span></a>),<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ABS.abs_defs.html#typ_e"><span class="id" title="inductive">typ_e</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#G5:10"><span class="id" title="variable">G5</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#e5:13"><span class="id" title="variable">e5</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#T5:14"><span class="id" title="variable">T5</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ABS.abs_defs.html#red_e"><span class="id" title="inductive">red_e</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#Flist:12"><span class="id" title="variable">Flist</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#s5:11"><span class="id" title="variable">s5</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#e5:13"><span class="id" title="variable">e5</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#s':15"><span class="id" title="variable">s'</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#e':16"><span class="id" title="variable">e'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">exists</span></a> <a id="G':17" class="idref" href="#G':17"><span class="id" title="binder">G'</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#subG"><span class="id" title="definition">subG</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#G5:10"><span class="id" title="variable">G5</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#G':17"><span class="id" title="variable">G'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">/\</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#G_vdash_s"><span class="id" title="definition">G_vdash_s</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#G':17"><span class="id" title="variable">G'</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#s':15"><span class="id" title="variable">s'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">/\</span></a> <a class="idref" href="ABS.abs_defs.html#typ_e"><span class="id" title="inductive">typ_e</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#G':17"><span class="id" title="variable">G'</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#e':16"><span class="id" title="variable">e'</span></a> <a class="idref" href="ABS.abs_functional_metatheory.html#T5:14"><span class="id" title="variable">T5</span></a>.<br/>
+<span class="id" title="keyword">Proof</span>.<br/>
+<span class="id" title="var">Admitted</span>.<br/>
+
+<br/>
+</div>
+</div>
+<div id="footer">
+  Generated by <a href="http://coq.inria.fr">coqdoc</a> and improved with <a href="https://github.com/palmskog/coqdocjs">CoqdocJS</a> as adapted for <a href="https://github.com/coq-community">coq-community</a>
+</div>
+</div>
+</body>
+
+</html>
diff --git a/docs/coqdoc/config.js b/docs/coqdoc/config.js
@@ -0,0 +1,79 @@
+var coqdocjs = coqdocjs || {};
+
+coqdocjs.repl = {
+    "forall": "∀",
+    "exists": "∃",
+    "~": "¬",
+    "/\\": "∧",
+    "\\/": "∨",
+    "->": "→",
+    "<-": "←",
+    "<->": "↔",
+    "=>": "⇒",
+    "<>": "≠",
+    "<=": "≤",
+    ">=": "≥",
+    "el": "∈",
+    "nel": "∉",
+    "<<=": "⊆",
+    "|-": "⊢",
+    ">>": "»",
+    "<<": "⊆",
+    "++": "⧺",
+    "===": "≡",
+    "=/=": "≢",
+    "=~=": "≅",
+    "==>": "⟹",
+    "<==": "⟸",
+    "False": "⊥",
+    "True": "⊤",
+    ":=": "≔",
+    "-|": "⊣",
+    "*": "×",
+    "::": "∷",
+    "lhd": "⊲",
+    "rhd": "⊳",
+    "nat": "ℕ",
+    "alpha": "α",
+    "beta": "β",
+    "gamma": "γ",
+    "delta": "δ",
+    "epsilon": "ε",
+    "eta": "η",
+    "iota": "ι",
+    "kappa": "κ",
+    "lambda": "λ",
+    "mu": "μ",
+    "nu": "ν",
+    "omega": "ω",
+    "phi": "ϕ",
+    "pi": "π",
+    "psi": "ψ",
+    "rho": "ρ",
+    "sigma": "σ",
+    "tau": "τ",
+    "theta": "θ",
+    "xi": "ξ",
+    "zeta": "ζ",
+    "Delta": "Δ",
+    "Gamma": "Γ",
+    "Pi": "Π",
+    "Sigma": "Σ",
+    "Omega": "Ω",
+    "Xi": "Ξ"
+};
+
+coqdocjs.subscr = {
+  "0" : "₀",
+  "1" : "₁",
+  "2" : "₂",
+  "3" : "₃",
+  "4" : "₄",
+  "5" : "₅",
+  "6" : "₆",
+  "7" : "₇",
+  "8" : "₈",
+  "9" : "₉",
+};
+
+coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="];
diff --git a/docs/coqdoc/coqdoc.css b/docs/coqdoc/coqdoc.css
@@ -0,0 +1,197 @@
+@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700);
+
+body{
+    font-family: 'Open Sans', sans-serif;
+    font-size: 14px;
+    color: #2D2D2D
+}
+
+a {
+    text-decoration: none;
+    border-radius: 3px;
+    padding-left: 3px;
+    padding-right: 3px;
+    margin-left: -3px;
+    margin-right: -3px;
+    color: inherit;
+    font-weight: bold;
+}
+
+#main .code a, #main .inlinecode a, #toc a {
+    font-weight: inherit;
+}
+
+a[href]:hover, [clickable]:hover{
+    background-color: rgba(0,0,0,0.1);
+    cursor: pointer;
+}
+
+h, h1, h2, h3, h4, h5 {
+    line-height: 1;
+    color: black;
+    text-rendering: optimizeLegibility;
+    font-weight: normal;
+    letter-spacing: 0.1em;
+    text-align: left;
+}
+
+div + br {
+  display: none;
+}
+
+div:empty{ display: none;}
+
+#main h1 {
+	font-size: 2em;
+}
+
+#main h2 {
+	font-size: 1.667rem;
+}
+
+#main h3 {
+	font-size: 1.333em;
+}
+
+#main h4, #main h5, #main h6 {
+	font-size: 1em;
+}
+
+#toc h2 {
+    padding-bottom: 0;
+}
+
+#main .doc {
+    margin: 0;
+    text-align: justify;
+}
+
+.inlinecode, .code, #main pre {
+    font-family: monospace;
+}
+
+.code > br:first-child {
+  display: none;
+}
+
+.doc + .code{
+  margin-top:0.5em;
+}
+
+.block{
+    display: block;
+    margin-top: 5px;
+    margin-bottom: 5px;
+    padding: 10px;
+    text-align: center;
+}
+
+.block img{
+    margin: 15px;
+}
+
+table.infrule {
+  border: 0px;
+  margin-left: 50px;
+  margin-top: 10px;
+  margin-bottom: 10px;
+}
+
+td.infrule {
+    font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace;
+    text-align: center;
+    padding: 0;
+    line-height: 1;
+}
+
+tr.infrulemiddle hr {
+    margin: 1px 0 1px 0;
+}
+
+.infrulenamecol {
+    color: rgb(60%,60%,60%);
+    padding-left: 1em;
+    padding-bottom: 0.1em
+}
+
+.id[type="constructor"], .id[type="projection"], .id[type="method"],
+.id[title="constructor"], .id[title="projection"], .id[title="method"]  {
+    color: #A30E16;
+}
+
+.id[type="var"], .id[type="variable"],
+.id[title="var"], .id[title="variable"] {
+    color: inherit;
+}
+
+.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"],
+.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] {
+    color: #A6650F;
+}
+
+.id[type="lemma"],
+.id[title="lemma"]{
+    color: #188B0C;
+}
+
+.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"],
+.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{
+ color : #2874AE;
+}
+
+.comment {
+  color: #808080;
+}
+
+/* TOC */
+
+#toc h2{
+  letter-spacing: 0;
+  font-size: 1.333em;
+}
+
+/* Index */
+
+#index {
+    margin: 0;
+    padding: 0;
+    width: 100%;
+}
+
+#index #frontispiece {
+    margin: 1em auto;
+    padding: 1em;
+    width: 60%;
+}
+
+.booktitle { font-size : 140%  }
+.authors { font-size : 90%;
+	         line-height: 115%;  }
+.moreauthors { font-size : 60%  }
+
+#index #entrance {
+    text-align: center;
+}
+
+#index #entrance .spacer {
+    margin: 0 30px 0 30px;
+}
+
+ul.doclist {
+    margin-top: 0em;
+    margin-bottom: 0em;
+}
+
+#toc > * {
+    clear: both;
+}
+
+#toc > a {
+    display: block;
+    float: left;
+    margin-top: 1em;
+}
+
+#toc a h2{
+    display: inline;
+}