Good

ianshil · Feb 29, 2024 · b37c542 · b37c542
1 parent d768f4d
commit b37c542
Show file tree

Hide file tree

Showing 18 changed files with 8,276 additions and 7 deletions.
diff --git a/Makefile b/Makefile
@@ -9,7 +9,6 @@ COQDOCFLAGS ?= \
   --index indexpage --no-lib-name --parse-comments \
   --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
 export COQDOCFLAGS
-PUBLIC_URL="https://ianshil.github.io/iS4"
 SUBDIR_ROOTS := theories
 DIRS := . $(shell find $(SUBDIR_ROOTS) -type d)
 
@@ -28,14 +27,8 @@ force $(COQ_PROJ) Makefile: ;
 %: $(COQMAKEFILE) force
 	@+$(MAKE) -f $< $@
 
-docian: makefile.coq
-	rm -fr html
-	@$(MAKE) -f makefile.coq html
-	cp resources/* html
-
 doc: makefile.coq
 	rm -fr html docs/*
-	COQDOCEXTRAFLAGS='--external $(PUBLIC_URL)'
 	@$(MAKE) -f makefile.coq html
 	cp html/* docs
 	cp $(EXTRA_DIR)/resources/* docs

diff --git a/html/GHC.iS4H.html b/html/GHC.iS4H.html
diff --git a/html/GHC.iS4H_logic.html b/html/GHC.iS4H_logic.html
diff --git a/html/GHC.iS4H_properties.html b/html/GHC.iS4H_properties.html
diff --git a/html/GHC.iS4_Lindenbaum_lem.html b/html/GHC.iS4_Lindenbaum_lem.html
diff --git a/html/GHC.iS4_enum.html b/html/GHC.iS4_enum.html
diff --git a/html/General.List_lemmasT.html b/html/General.List_lemmasT.html
diff --git a/html/General.existsT.html b/html/General.existsT.html
@@ -0,0 +1,49 @@
+<!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="resources/coqdoc.css" rel="stylesheet" type="text/css" />
+<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
+<script type="text/javascript" src="resources/config.js"></script>
+<script type="text/javascript" src="resources/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/ianshil/iS4">Project Page</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">
+<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/distrib/V8.18.0/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/distrib/V8.18.0/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/distrib/V8.18.0/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/distrib/V8.18.0/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>
diff --git a/html/General.gen.html b/html/General.gen.html
diff --git a/html/General.genT.html b/html/General.genT.html
diff --git a/html/General.general_export.html b/html/General.general_export.html
@@ -0,0 +1,43 @@
+<!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="resources/coqdoc.css" rel="stylesheet" type="text/css" />
+<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
+<script type="text/javascript" src="resources/config.js"></script>
+<script type="text/javascript" src="resources/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/ianshil/iS4">Project Page</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">
+<h1 class="libtitle">General.general_export</h1>
+
+<div class="code">
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="General.List_lemmasT.html#"><span class="id" title="library">List_lemmasT</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="General.existsT.html#"><span class="id" title="library">existsT</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="General.gen.html#"><span class="id" title="library">gen</span></a>.<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="General.genT.html#"><span class="id" title="library">genT</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>