pagina

gonzigaran · Apr 4, 2024 · 99fae86 · 99fae86
1 parent cacc2cc
commit 99fae86
Show file tree

Hide file tree

Showing 120 changed files with 372 additions and 122 deletions.
diff --git a/docs/Agda.Builtin.Bool.html b/docs/Agda.Builtin.Bool.html
@@ -1,4 +1,5 @@
-<a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-universe-polymorphism</a>
+<!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">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-universe-polymorphism</a>
             <a id="80" class="Pragma">--no-sized-types</a> <a id="97" class="Pragma">--no-guardedness</a> <a id="114" class="Symbol">#-}</a>
 
 <a id="119" class="Keyword">module</a> <a id="126" href="Agda.Builtin.Bool.html" class="Module">Agda.Builtin.Bool</a> <a id="144" class="Keyword">where</a>
@@ -13,3 +14,4 @@
 <a id="279" class="Symbol">{-#</a> <a id="283" class="Keyword">COMPILE</a> <a id="291" class="Keyword">JS</a> <a id="294" href="Agda.Builtin.Bool.html#156" class="Datatype">Bool</a>  <a id="300" class="Pragma">=</a> <a id="302" class="Pragma">function</a> <a id="311" class="Pragma">(x,v)</a> <a id="317" class="Pragma">{</a> <a id="319" class="Pragma">return</a> <a id="326" class="Pragma">((x)?</a> <a id="332" class="Pragma">v[&quot;true&quot;]()</a> <a id="344" class="Pragma">:</a> <a id="346" class="Pragma">v[&quot;false&quot;]());</a> <a id="361" class="Pragma">}</a> <a id="363" class="Symbol">#-}</a>
 <a id="367" class="Symbol">{-#</a> <a id="371" class="Keyword">COMPILE</a> <a id="379" class="Keyword">JS</a> <a id="382" href="Agda.Builtin.Bool.html#175" class="InductiveConstructor">false</a> <a id="388" class="Pragma">=</a> <a id="390" class="Pragma">false</a> <a id="396" class="Symbol">#-}</a>
 <a id="400" class="Symbol">{-#</a> <a id="404" class="Keyword">COMPILE</a> <a id="412" class="Keyword">JS</a> <a id="415" href="Agda.Builtin.Bool.html#181" class="InductiveConstructor">true</a>  <a id="421" class="Pragma">=</a> <a id="423" class="Pragma">true</a>  <a id="429" class="Symbol">#-}</a>
+</pre></body></html>
diff --git a/docs/Agda.Builtin.Equality.html b/docs/Agda.Builtin.Equality.html
@@ -1,4 +1,5 @@
-<a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-sized-types</a> <a id="58" class="Pragma">--no-guardedness</a> <a id="75" class="Symbol">#-}</a>
+<!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">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-sized-types</a> <a id="58" class="Pragma">--no-guardedness</a> <a id="75" class="Symbol">#-}</a>
 
 <a id="80" class="Keyword">module</a> <a id="87" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a> <a id="109" class="Keyword">where</a>
 
@@ -7,3 +8,4 @@
   <a id="181" class="Keyword">instance</a> <a id="_≡_.refl"></a><a id="190" href="Agda.Builtin.Equality.html#190" class="InductiveConstructor">refl</a> <a id="195" class="Symbol">:</a> <a id="197" href="Agda.Builtin.Equality.html#154" class="Bound">x</a> <a id="199" href="Agda.Builtin.Equality.html#133" class="Datatype Operator">≡</a> <a id="201" href="Agda.Builtin.Equality.html#154" class="Bound">x</a>
 
 <a id="204" class="Symbol">{-#</a> <a id="208" class="Keyword">BUILTIN</a> <a id="216" class="Keyword">EQUALITY</a> <a id="225" href="Agda.Builtin.Equality.html#133" class="Datatype Operator">_≡_</a> <a id="229" class="Symbol">#-}</a>
+</pre></body></html>
diff --git a/docs/Agda.Builtin.Maybe.html b/docs/Agda.Builtin.Maybe.html
@@ -1,4 +1,5 @@
-<a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-sized-types</a> <a id="58" class="Pragma">--no-guardedness</a> <a id="75" class="Symbol">#-}</a>
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Agda.Builtin.Maybe</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-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-sized-types</a> <a id="58" class="Pragma">--no-guardedness</a> <a id="75" class="Symbol">#-}</a>
 
 <a id="80" class="Keyword">module</a> <a id="87" href="Agda.Builtin.Maybe.html" class="Module">Agda.Builtin.Maybe</a> <a id="106" class="Keyword">where</a>
 
@@ -7,3 +8,4 @@
   <a id="Maybe.nothing"></a><a id="177" href="Agda.Builtin.Maybe.html#177" class="InductiveConstructor">nothing</a> <a id="185" class="Symbol">:</a> <a id="187" href="Agda.Builtin.Maybe.html#118" class="Datatype">Maybe</a> <a id="193" href="Agda.Builtin.Maybe.html#129" class="Bound">A</a>
 
 <a id="196" class="Symbol">{-#</a> <a id="200" class="Keyword">BUILTIN</a> <a id="208" class="Keyword">MAYBE</a> <a id="214" href="Agda.Builtin.Maybe.html#118" class="Datatype">Maybe</a> <a id="220" class="Symbol">#-}</a>
+</pre></body></html>
diff --git a/docs/Agda.Builtin.Nat.html b/docs/Agda.Builtin.Nat.html
@@ -1,4 +1,5 @@
-<a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-universe-polymorphism</a>
+<!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">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-universe-polymorphism</a>
             <a id="80" class="Pragma">--no-sized-types</a> <a id="97" class="Pragma">--no-guardedness</a> <a id="114" class="Symbol">#-}</a>
 
 <a id="119" class="Keyword">module</a> <a id="126" href="Agda.Builtin.Nat.html" class="Module">Agda.Builtin.Nat</a> <a id="143" class="Keyword">where</a>
@@ -132,3 +133,4 @@
 <a id="3955" class="Comment">--           = ((1 + n) + k) mod (1 + m)       by commutativity</a>
 <a id="4019" class="Comment">--</a>
 <a id="4022" class="Comment">-- Q.e.d.</a>
+</pre></body></html>
diff --git a/docs/Agda.Builtin.Sigma.html b/docs/Agda.Builtin.Sigma.html
@@ -1,4 +1,5 @@
-<a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-sized-types</a> <a id="58" class="Pragma">--no-guardedness</a> <a id="75" class="Symbol">#-}</a>
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Agda.Builtin.Sigma</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-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-sized-types</a> <a id="58" class="Pragma">--no-guardedness</a> <a id="75" class="Symbol">#-}</a>
 
 <a id="80" class="Keyword">module</a> <a id="87" href="Agda.Builtin.Sigma.html" class="Module">Agda.Builtin.Sigma</a> <a id="106" class="Keyword">where</a>
 
@@ -15,3 +16,4 @@
 <a id="274" class="Keyword">infixr</a> <a id="281" class="Number">4</a> <a id="283" href="Agda.Builtin.Sigma.html#218" class="InductiveConstructor Operator">_,_</a>
 
 <a id="288" class="Symbol">{-#</a> <a id="292" class="Keyword">BUILTIN</a> <a id="300" class="Keyword">SIGMA</a> <a id="306" href="Agda.Builtin.Sigma.html#148" class="Record">Σ</a> <a id="308" class="Symbol">#-}</a>
+</pre></body></html>
diff --git a/docs/Agda.Builtin.Strict.html b/docs/Agda.Builtin.Strict.html
@@ -1,4 +1,5 @@
-<a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-sized-types</a> <a id="58" class="Pragma">--no-guardedness</a> <a id="75" class="Symbol">#-}</a>
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Agda.Builtin.Strict</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-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-sized-types</a> <a id="58" class="Pragma">--no-guardedness</a> <a id="75" class="Symbol">#-}</a>
 
 <a id="80" class="Keyword">module</a> <a id="87" href="Agda.Builtin.Strict.html" class="Module">Agda.Builtin.Strict</a> <a id="107" class="Keyword">where</a>
 
@@ -7,3 +8,4 @@
 <a id="149" class="Keyword">primitive</a>
   <a id="primForce"></a><a id="161" href="Agda.Builtin.Strict.html#161" class="Primitive">primForce</a>      <a id="176" class="Symbol">:</a> <a id="178" class="Symbol">∀</a> <a id="180" class="Symbol">{</a><a id="181" href="Agda.Builtin.Strict.html#181" class="Bound">a</a> <a id="183" href="Agda.Builtin.Strict.html#183" class="Bound">b</a><a id="184" class="Symbol">}</a> <a id="186" class="Symbol">{</a><a id="187" href="Agda.Builtin.Strict.html#187" class="Bound">A</a> <a id="189" class="Symbol">:</a> <a id="191" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="195" href="Agda.Builtin.Strict.html#181" class="Bound">a</a><a id="196" class="Symbol">}</a> <a id="198" class="Symbol">{</a><a id="199" href="Agda.Builtin.Strict.html#199" class="Bound">B</a> <a id="201" class="Symbol">:</a> <a id="203" href="Agda.Builtin.Strict.html#187" class="Bound">A</a> <a id="205" class="Symbol">→</a> <a id="207" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="211" href="Agda.Builtin.Strict.html#183" class="Bound">b</a><a id="212" class="Symbol">}</a> <a id="214" class="Symbol">(</a><a id="215" href="Agda.Builtin.Strict.html#215" class="Bound">x</a> <a id="217" class="Symbol">:</a> <a id="219" href="Agda.Builtin.Strict.html#187" class="Bound">A</a><a id="220" class="Symbol">)</a> <a id="222" class="Symbol">→</a> <a id="224" class="Symbol">(∀</a> <a id="227" href="Agda.Builtin.Strict.html#227" class="Bound">x</a> <a id="229" class="Symbol">→</a> <a id="231" href="Agda.Builtin.Strict.html#199" class="Bound">B</a> <a id="233" href="Agda.Builtin.Strict.html#227" class="Bound">x</a><a id="234" class="Symbol">)</a> <a id="236" class="Symbol">→</a> <a id="238" href="Agda.Builtin.Strict.html#199" class="Bound">B</a> <a id="240" href="Agda.Builtin.Strict.html#215" class="Bound">x</a>
   <a id="primForceLemma"></a><a id="244" href="Agda.Builtin.Strict.html#244" class="Primitive">primForceLemma</a> <a id="259" class="Symbol">:</a> <a id="261" class="Symbol">∀</a> <a id="263" class="Symbol">{</a><a id="264" href="Agda.Builtin.Strict.html#264" class="Bound">a</a> <a id="266" href="Agda.Builtin.Strict.html#266" class="Bound">b</a><a id="267" class="Symbol">}</a> <a id="269" class="Symbol">{</a><a id="270" href="Agda.Builtin.Strict.html#270" class="Bound">A</a> <a id="272" class="Symbol">:</a> <a id="274" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="278" href="Agda.Builtin.Strict.html#264" class="Bound">a</a><a id="279" class="Symbol">}</a> <a id="281" class="Symbol">{</a><a id="282" href="Agda.Builtin.Strict.html#282" class="Bound">B</a> <a id="284" class="Symbol">:</a> <a id="286" href="Agda.Builtin.Strict.html#270" class="Bound">A</a> <a id="288" class="Symbol">→</a> <a id="290" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="294" href="Agda.Builtin.Strict.html#266" class="Bound">b</a><a id="295" class="Symbol">}</a> <a id="297" class="Symbol">(</a><a id="298" href="Agda.Builtin.Strict.html#298" class="Bound">x</a> <a id="300" class="Symbol">:</a> <a id="302" href="Agda.Builtin.Strict.html#270" class="Bound">A</a><a id="303" class="Symbol">)</a> <a id="305" class="Symbol">(</a><a id="306" href="Agda.Builtin.Strict.html#306" class="Bound">f</a> <a id="308" class="Symbol">:</a> <a id="310" class="Symbol">∀</a> <a id="312" href="Agda.Builtin.Strict.html#312" class="Bound">x</a> <a id="314" class="Symbol">→</a> <a id="316" href="Agda.Builtin.Strict.html#282" class="Bound">B</a> <a id="318" href="Agda.Builtin.Strict.html#312" class="Bound">x</a><a id="319" class="Symbol">)</a> <a id="321" class="Symbol">→</a> <a id="323" href="Agda.Builtin.Strict.html#161" class="Primitive">primForce</a> <a id="333" href="Agda.Builtin.Strict.html#298" class="Bound">x</a> <a id="335" href="Agda.Builtin.Strict.html#306" class="Bound">f</a> <a id="337" href="Agda.Builtin.Equality.html#133" class="Datatype Operator">≡</a> <a id="339" href="Agda.Builtin.Strict.html#306" class="Bound">f</a> <a id="341" href="Agda.Builtin.Strict.html#298" class="Bound">x</a>
+</pre></body></html>
diff --git a/docs/Agda.Builtin.Unit.html b/docs/Agda.Builtin.Unit.html
@@ -1,4 +1,5 @@
-<a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-universe-polymorphism</a>
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Agda.Builtin.Unit</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-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-universe-polymorphism</a>
             <a id="80" class="Pragma">--no-sized-types</a> <a id="97" class="Pragma">--no-guardedness</a> <a id="114" class="Symbol">#-}</a>
 
 <a id="119" class="Keyword">module</a> <a id="126" href="Agda.Builtin.Unit.html" class="Module">Agda.Builtin.Unit</a> <a id="144" class="Keyword">where</a>
@@ -8,3 +9,4 @@
 
 <a id="199" class="Symbol">{-#</a> <a id="203" class="Keyword">BUILTIN</a> <a id="211" class="Keyword">UNIT</a> <a id="216" href="Agda.Builtin.Unit.html#158" class="Record">⊤</a> <a id="218" class="Symbol">#-}</a>
 <a id="222" class="Symbol">{-#</a> <a id="226" class="Keyword">COMPILE</a> <a id="234" class="Keyword">GHC</a> <a id="238" href="Agda.Builtin.Unit.html#158" class="Record">⊤</a> <a id="240" class="Pragma">=</a> <a id="242" class="Pragma">data</a> <a id="247" class="Pragma">()</a> <a id="250" class="Pragma">(())</a> <a id="255" class="Symbol">#-}</a>
+</pre></body></html>
diff --git a/docs/Agda.Primitive.html b/docs/Agda.Primitive.html
@@ -1,4 +1,5 @@
-<a id="1" class="Comment">-- The Agda primitives (preloaded).</a>
+<!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">--cubical-compatible</a> <a id="71" class="Pragma">--no-import-sorts</a> <a id="89" class="Symbol">#-}</a>
 
@@ -35,3 +36,4 @@
 <a id="837" class="Symbol">{-#</a> <a id="841" class="Keyword">BUILTIN</a> <a id="849" class="Keyword">LEVELZERO</a> <a id="859" href="Agda.Primitive.html#758" class="Primitive">lzero</a> <a id="865" class="Symbol">#-}</a>
 <a id="869" class="Symbol">{-#</a> <a id="873" class="Keyword">BUILTIN</a> <a id="881" class="Keyword">LEVELSUC</a>  <a id="891" href="Agda.Primitive.html#774" class="Primitive">lsuc</a>  <a id="897" class="Symbol">#-}</a>
 <a id="901" class="Symbol">{-#</a> <a id="905" class="Keyword">BUILTIN</a> <a id="913" class="Keyword">LEVELMAX</a>  <a id="923" href="Agda.Primitive.html#804" class="Primitive Operator">_⊔_</a>   <a id="929" class="Symbol">#-}</a>
+</pre></body></html>
diff --git a/docs/Algebra.Bundles.html b/docs/Algebra.Bundles.html
@@ -1,4 +1,5 @@
-<a id="1" class="Comment">------------------------------------------------------------------------</a>
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Algebra.Bundles</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
 <a id="74" class="Comment">-- The Agda standard library</a>
 <a id="103" class="Comment">--</a>
 <a id="106" class="Comment">-- Definitions of algebraic structures like monoids and rings</a>
@@ -930,3 +931,4 @@
 <a id="24156" class="String">&quot;Warning: RawSemigroup was deprecated in v1.0.
 Please use RawMagma instead.&quot;</a>
 <a id="24233" class="Symbol">#-}</a>
+</pre></body></html>
diff --git a/docs/Algebra.Consequences.Base.html b/docs/Algebra.Consequences.Base.html
@@ -1,4 +1,5 @@
-<a id="1" class="Comment">------------------------------------------------------------------------</a>
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Algebra.Consequences.Base</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
 <a id="74" class="Comment">-- The Agda standard library</a>
 <a id="103" class="Comment">--</a>
 <a id="106" class="Comment">-- Lemmas relating algebraic definitions (such as associativity and</a>
@@ -20,3 +21,4 @@
 <a id="634" href="Algebra.Consequences.Base.html#535" class="Function">sel⇒idem</a> <a id="643" class="Symbol">_</a> <a id="645" href="Algebra.Consequences.Base.html#645" class="Bound">sel</a> <a id="649" href="Algebra.Consequences.Base.html#649" class="Bound">x</a> <a id="651" class="Keyword">with</a> <a id="656" href="Algebra.Consequences.Base.html#645" class="Bound">sel</a> <a id="660" href="Algebra.Consequences.Base.html#649" class="Bound">x</a> <a id="662" href="Algebra.Consequences.Base.html#649" class="Bound">x</a>
 <a id="664" class="Symbol">...</a> <a id="668" class="Symbol">|</a> <a id="670" href="Data.Sum.Base.html#793" class="InductiveConstructor">inj₁</a> <a id="675" href="Algebra.Consequences.Base.html#675" class="Bound">x•x≈x</a> <a id="681" class="Symbol">=</a> <a id="683" href="Algebra.Consequences.Base.html#675" class="Bound">x•x≈x</a>
 <a id="689" class="Symbol">...</a> <a id="693" class="Symbol">|</a> <a id="695" href="Data.Sum.Base.html#818" class="InductiveConstructor">inj₂</a> <a id="700" href="Algebra.Consequences.Base.html#700" class="Bound">x•x≈x</a> <a id="706" class="Symbol">=</a> <a id="708" href="Algebra.Consequences.Base.html#700" class="Bound">x•x≈x</a>
+</pre></body></html>