1 files changed, 35 insertions, 0 deletions
diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html
new file mode 100644
index 0000000..5829754
--- /dev/null
+++ b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html
@@ -0,0 +1,35 @@
+<!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>
+
+<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="Symbol">#-}</a>
+
+<a id="82" class="Keyword">module</a> <a id="89" href="Agda.Primitive.html" class="Module">Agda.Primitive</a> <a id="104" class="Keyword">where</a>
+
+<a id="111" class="Comment">------------------------------------------------------------------------</a>
+<a id="184" class="Comment">-- Universe levels</a>
+<a id="203" class="Comment">------------------------------------------------------------------------</a>
+
+<a id="277" class="Keyword">infixl</a> <a id="284" class="Number">6</a> <a id="286" href="Agda.Primitive.html#636" class="Primitive Operator">_⊔_</a>
+
+<a id="291" class="Comment">-- Level is the first thing we need to define.</a>
+<a id="338" class="Comment">-- The other postulates can only be checked if built-in Level is known.</a>
+
+<a id="411" class="Keyword">postulate</a>
+  <a id="Level"></a><a id="423" href="Agda.Primitive.html#423" class="Postulate">Level</a> <a id="429" class="Symbol">:</a> <a id="431" class="PrimitiveType">Set</a>
+
+<a id="436" class="Comment">-- MAlonzo compiles Level to (). This should be safe, because it is</a>
+<a id="504" class="Comment">-- not possible to pattern match on levels.</a>
+
+<a id="549" class="Symbol">{-#</a> <a id="553" class="Keyword">BUILTIN</a> <a id="561" class="Keyword">LEVEL</a> <a id="567" href="Agda.Primitive.html#423" class="Postulate">Level</a> <a id="573" class="Symbol">#-}</a>
+
+<a id="578" class="Keyword">postulate</a>
+  <a id="lzero"></a><a id="590" href="Agda.Primitive.html#590" class="Postulate">lzero</a> <a id="596" class="Symbol">:</a> <a id="598" href="Agda.Primitive.html#423" class="Postulate">Level</a>
+  <a id="lsuc"></a><a id="606" href="Agda.Primitive.html#606" class="Postulate">lsuc</a>  <a id="612" class="Symbol">:</a> <a id="614" class="Symbol">(</a><a id="615" href="Agda.Primitive.html#615" class="Bound">ℓ</a> <a id="617" class="Symbol">:</a> <a id="619" href="Agda.Primitive.html#423" class="Postulate">Level</a><a id="624" class="Symbol">)</a> <a id="626" class="Symbol">→</a> <a id="628" href="Agda.Primitive.html#423" class="Postulate">Level</a>
+  <a id="_⊔_"></a><a id="636" href="Agda.Primitive.html#636" class="Postulate Operator">_⊔_</a>   <a id="642" class="Symbol">:</a> <a id="644" class="Symbol">(</a><a id="645" href="Agda.Primitive.html#645" class="Bound">ℓ₁</a> <a id="648" href="Agda.Primitive.html#648" class="Bound">ℓ₂</a> <a id="651" class="Symbol">:</a> <a id="653" href="Agda.Primitive.html#423" class="Postulate">Level</a><a id="658" class="Symbol">)</a> <a id="660" class="Symbol">→</a> <a id="662" href="Agda.Primitive.html#423" class="Postulate">Level</a>
+
+<a id="669" class="Symbol">{-#</a> <a id="673" class="Keyword">BUILTIN</a> <a id="681" class="Keyword">LEVELZERO</a> <a id="691" href="Agda.Primitive.html#590" class="Primitive">lzero</a> <a id="697" class="Symbol">#-}</a>
+<a id="701" class="Symbol">{-#</a> <a id="705" class="Keyword">BUILTIN</a> <a id="713" class="Keyword">LEVELSUC</a>  <a id="723" href="Agda.Primitive.html#606" class="Primitive">lsuc</a>  <a id="729" class="Symbol">#-}</a>
+<a id="733" class="Symbol">{-#</a> <a id="737" class="Keyword">BUILTIN</a> <a id="745" class="Keyword">LEVELMAX</a>  <a id="755" href="Agda.Primitive.html#636" class="Primitive Operator">_⊔_</a>   <a id="761" class="Symbol">#-}</a>
+
+<a id="766" class="Symbol">{-#</a> <a id="770" class="Keyword">BUILTIN</a> <a id="778" class="Keyword">SETOMEGA</a> <a id="Setω"></a><a id="787" href="Agda.Primitive.html#787" class="Primitive">Setω</a> <a id="792" class="Symbol">#-}</a>
+</pre></body></html>
+\ No newline at end of file