foo

jonsterling · Sep 21, 2020 · 815f567 · 815f567
1 parent c7f2cb3
commit 815f567
Show file tree

Hide file tree

Showing 21 changed files with 73 additions and 19 deletions.
diff --git a/build.sh b/build.sh
@@ -1,3 +1,3 @@
 #!/bin/bash 
 
-agda --html-dir=docs --html src/index.agda
+agda --html-dir=docs --css style.css --html src/index.agda
diff --git a/docs/Agda.Builtin.Bool.html b/docs/Agda.Builtin.Bool.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Agda.Builtin.Bool</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Pragma">--safe</a> <a id="32" class="Pragma">--no-universe-polymorphism</a>
+<html><head><meta charset="utf-8"><title>Agda.Builtin.Bool</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Pragma">--safe</a> <a id="32" class="Pragma">--no-universe-polymorphism</a>
             <a id="71" class="Pragma">--no-sized-types</a> <a id="88" class="Pragma">--no-guardedness</a>  <a id="106" class="Pragma">--no-subtyping</a> <a id="121" class="Symbol">#-}</a>
 
 <a id="126" class="Keyword">module</a> <a id="133" href="Agda.Builtin.Bool.html" class="Module">Agda.Builtin.Bool</a> <a id="151" class="Keyword">where</a>

diff --git a/docs/Agda.Builtin.Equality.html b/docs/Agda.Builtin.Equality.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Agda.Builtin.Equality</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Pragma">--safe</a> <a id="32" class="Pragma">--no-sized-types</a> <a id="49" class="Pragma">--no-guardedness</a>
+<html><head><meta charset="utf-8"><title>Agda.Builtin.Equality</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Pragma">--safe</a> <a id="32" class="Pragma">--no-sized-types</a> <a id="49" class="Pragma">--no-guardedness</a>
             <a id="78" class="Pragma">--no-subtyping</a> <a id="93" class="Symbol">#-}</a>
 
 <a id="98" class="Keyword">module</a> <a id="105" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a> <a id="127" class="Keyword">where</a>

diff --git a/docs/Agda.Builtin.List.html b/docs/Agda.Builtin.List.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Agda.Builtin.List</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Pragma">--safe</a> <a id="32" class="Pragma">--no-sized-types</a> <a id="49" class="Pragma">--no-guardedness</a>
+<html><head><meta charset="utf-8"><title>Agda.Builtin.List</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Pragma">--safe</a> <a id="32" class="Pragma">--no-sized-types</a> <a id="49" class="Pragma">--no-guardedness</a>
             <a id="78" class="Pragma">--no-subtyping</a> <a id="93" class="Symbol">#-}</a>
 
 <a id="98" class="Keyword">module</a> <a id="105" href="Agda.Builtin.List.html" class="Module">Agda.Builtin.List</a> <a id="123" class="Keyword">where</a>

diff --git a/docs/Agda.Builtin.Nat.html b/docs/Agda.Builtin.Nat.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Agda.Builtin.Nat</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Pragma">--safe</a> <a id="32" class="Pragma">--no-universe-polymorphism</a>
+<html><head><meta charset="utf-8"><title>Agda.Builtin.Nat</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Pragma">--safe</a> <a id="32" class="Pragma">--no-universe-polymorphism</a>
             <a id="71" class="Pragma">--no-sized-types</a> <a id="88" class="Pragma">--no-guardedness</a> <a id="105" class="Pragma">--no-subtyping</a> <a id="120" class="Symbol">#-}</a>
 
 <a id="125" class="Keyword">module</a> <a id="132" href="Agda.Builtin.Nat.html" class="Module">Agda.Builtin.Nat</a> <a id="149" class="Keyword">where</a>

diff --git a/docs/Agda.Primitive.Cubical.html b/docs/Agda.Primitive.Cubical.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Agda.Primitive.Cubical</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical</a> <a id="23" class="Pragma">--no-subtyping</a> <a id="38" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>Agda.Primitive.Cubical</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical</a> <a id="23" class="Pragma">--no-subtyping</a> <a id="38" class="Symbol">#-}</a>
 
 <a id="43" class="Keyword">module</a> <a id="50" href="Agda.Primitive.Cubical.html" class="Module">Agda.Primitive.Cubical</a> <a id="73" class="Keyword">where</a>
 

diff --git a/docs/Agda.Primitive.html b/docs/Agda.Primitive.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Agda.Primitive</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- The Agda primitives (preloaded).</a>
+<html><head><meta charset="utf-8"><title>Agda.Primitive</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- The Agda primitives (preloaded).</a>
 
 <a id="38" class="Symbol">{-#</a> <a id="42" class="Keyword">OPTIONS</a> <a id="50" class="Pragma">--without-K</a> <a id="62" class="Pragma">--no-subtyping</a> <a id="77" class="Pragma">--no-import-sorts</a> <a id="95" class="Symbol">#-}</a>
 

diff --git a/docs/BarTheorem.html b/docs/BarTheorem.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>BarTheorem</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>BarTheorem</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
 
 <a id="30" class="Keyword">module</a> <a id="37" href="BarTheorem.html" class="Module">BarTheorem</a> <a id="48" class="Keyword">where</a>
 

diff --git a/docs/Basis.html b/docs/Basis.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Basis</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- Authors: Darin Morrison, Jon Sterling</a>
+<html><head><meta charset="utf-8"><title>Basis</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- Authors: Darin Morrison, Jon Sterling</a>
 
 <a id="43" class="Symbol">{-#</a> <a id="47" class="Keyword">OPTIONS</a> <a id="55" class="Pragma">--without-K</a> <a id="67" class="Symbol">#-}</a>
 

diff --git a/docs/Dialogue.Core.html b/docs/Dialogue.Core.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Dialogue.Core</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>Dialogue.Core</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
 
 <a id="30" class="Keyword">module</a> <a id="37" href="Dialogue.Core.html" class="Module">Dialogue.Core</a> <a id="51" class="Keyword">where</a>
 

diff --git a/docs/Dialogue.Normalize.html b/docs/Dialogue.Normalize.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Dialogue.Normalize</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>Dialogue.Normalize</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
 
 <a id="30" class="Keyword">module</a> <a id="37" href="Dialogue.Normalize.html" class="Module">Dialogue.Normalize</a> <a id="56" class="Keyword">where</a>
 

diff --git a/docs/Dialogue.html b/docs/Dialogue.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Dialogue</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>Dialogue</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
 
 <a id="30" class="Keyword">module</a> <a id="37" href="Dialogue.html" class="Module">Dialogue</a> <a id="46" class="Keyword">where</a>
 

diff --git a/docs/Securability.html b/docs/Securability.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Securability</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>Securability</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
 
 <a id="30" class="Keyword">module</a> <a id="37" href="Securability.html" class="Module">Securability</a> <a id="50" class="Keyword">where</a>
 

diff --git a/docs/Spread.Baire.html b/docs/Spread.Baire.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Spread.Baire</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>Spread.Baire</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
 
 <a id="30" class="Keyword">module</a> <a id="37" href="Spread.Baire.html" class="Module">Spread.Baire</a> <a id="50" class="Keyword">where</a>
 

diff --git a/docs/Spread.Core.html b/docs/Spread.Core.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>Spread.Core</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>Spread.Core</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
 
 <a id="30" class="Keyword">module</a> <a id="37" href="Spread.Core.html" class="Module">Spread.Core</a> <a id="49" class="Symbol">(</a><a id="50" href="Spread.Core.html#50" class="Bound">X</a> <a id="52" class="Symbol">:</a> <a id="54" href="Agda.Primitive.html#326" class="Primitive">Set</a><a id="57" class="Symbol">)</a> <a id="59" class="Keyword">where</a>
 

diff --git a/docs/SystemT.Context.html b/docs/SystemT.Context.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>SystemT.Context</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>SystemT.Context</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
 
 <a id="30" class="Keyword">module</a> <a id="37" href="SystemT.Context.html" class="Module">SystemT.Context</a> <a id="53" class="Keyword">where</a>
 

diff --git a/docs/SystemT.Semantics.html b/docs/SystemT.Semantics.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>SystemT.Semantics</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>SystemT.Semantics</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
 
 <a id="30" class="Keyword">module</a> <a id="37" href="SystemT.Semantics.html" class="Module">SystemT.Semantics</a> <a id="55" class="Keyword">where</a>
 

diff --git a/docs/SystemT.Syntax.html b/docs/SystemT.Syntax.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>SystemT.Syntax</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>SystemT.Syntax</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
 
 <a id="30" class="Keyword">module</a> <a id="37" href="SystemT.Syntax.html" class="Module">SystemT.Syntax</a> <a id="52" class="Keyword">where</a>
 

diff --git a/docs/index.html b/docs/index.html
@@ -1,5 +1,5 @@
 <!DOCTYPE HTML>
-<html><head><meta charset="utf-8"><title>index</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
+<html><head><meta charset="utf-8"><title>index</title><link rel="stylesheet" href="style.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Symbol">#-}</a>
 
 <a id="30" class="Comment">-- This is the formalization of the paper &quot;Higher-Order Functions and</a>
 <a id="100" class="Comment">-- Brouwer&#39;s Thesis&quot; by Sterling.</a>

diff --git a/docs/pragmatapro.css b/docs/pragmatapro.css
diff --git a/docs/style.css b/docs/style.css
@@ -0,0 +1,48 @@
+@import 'pragmatapro.css';
+
+pre {
+  font-family: 'Pragmata Pro Mono';
+  font-size: 10pt;
+}
+
+/* Aspects. */
+.Agda .Comment       { color: #B22222 }
+.Agda .Background    {}
+.Agda .Markup        { color: #000000 }
+.Agda .Keyword       { color: #CD6600 }
+.Agda .String        { color: #B22222 }
+.Agda .Number        { color: #A020F0 }
+.Agda .Symbol        { color: #404040 }
+.Agda .PrimitiveType { color: #0000CD }
+.Agda .Pragma        { color: black   }
+.Agda .Operator      {}
+
+/* NameKinds. */
+.Agda .Bound                  { color: black   }
+.Agda .Generalizable          { color: black   }
+.Agda .InductiveConstructor   { color: #008B00 }
+.Agda .CoinductiveConstructor { color: #8B7500 }
+.Agda .Datatype               { color: #0000CD }
+.Agda .Field                  { color: #EE1289 }
+.Agda .Function               { color: #0000CD }
+.Agda .Module                 { color: #A020F0 }
+.Agda .Postulate              { color: #0000CD }
+.Agda .Primitive              { color: #0000CD }
+.Agda .Record                 { color: #0000CD }
+
+/* OtherAspects. */
+.Agda .DottedPattern        {}
+.Agda .UnsolvedMeta         { color: black; background: yellow         }
+.Agda .UnsolvedConstraint   { color: black; background: yellow         }
+.Agda .TerminationProblem   { color: black; background: #FFA07A        }
+.Agda .IncompletePattern    { color: black; background: #F5DEB3        }
+.Agda .Error                { color: red;   text-decoration: underline }
+.Agda .TypeChecks           { color: black; background: #ADD8E6        }
+.Agda .Deadcode             { color: black; background: #808080        }
+.Agda .ShadowingInTelescope { color: black; background: #808080        }
+
+/* Standard attributes. */
+.Agda a { text-decoration: none }
+.Agda a[href]:hover { background-color: #B4EEB4 }
+.Agda [href].hover-highlight { background-color: #B4EEB4; }
+