prueba pagina clones

gonzigaran · Apr 4, 2024 · 8622d71 · 8622d71
1 parent 607a809
commit 8622d71
Show file tree

Hide file tree

Showing 129 changed files with 19,133 additions and 0 deletions.
diff --git a/docs/Agda.Builtin.Bool.html b/docs/Agda.Builtin.Bool.html
@@ -0,0 +1,15 @@
+<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>
+
+<a id="151" class="Keyword">data</a> <a id="Bool"></a><a id="156" href="Agda.Builtin.Bool.html#156" class="Datatype">Bool</a> <a id="161" class="Symbol">:</a> <a id="163" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="167" class="Keyword">where</a>
+  <a id="Bool.false"></a><a id="175" href="Agda.Builtin.Bool.html#175" class="InductiveConstructor">false</a> <a id="Bool.true"></a><a id="181" href="Agda.Builtin.Bool.html#181" class="InductiveConstructor">true</a> <a id="186" class="Symbol">:</a> <a id="188" href="Agda.Builtin.Bool.html#156" class="Datatype">Bool</a>
+
+<a id="194" class="Symbol">{-#</a> <a id="198" class="Keyword">BUILTIN</a> <a id="206" class="Keyword">BOOL</a>  <a id="212" href="Agda.Builtin.Bool.html#156" class="Datatype">Bool</a>  <a id="218" class="Symbol">#-}</a>
+<a id="222" class="Symbol">{-#</a> <a id="226" class="Keyword">BUILTIN</a> <a id="234" class="Keyword">FALSE</a> <a id="240" href="Agda.Builtin.Bool.html#175" class="InductiveConstructor">false</a> <a id="246" class="Symbol">#-}</a>
+<a id="250" class="Symbol">{-#</a> <a id="254" class="Keyword">BUILTIN</a> <a id="262" class="Keyword">TRUE</a>  <a id="268" href="Agda.Builtin.Bool.html#181" class="InductiveConstructor">true</a>  <a id="274" class="Symbol">#-}</a>
+
+<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>
diff --git a/docs/Agda.Builtin.Equality.html b/docs/Agda.Builtin.Equality.html
@@ -0,0 +1,9 @@
+<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>
+
+<a id="116" class="Keyword">infix</a> <a id="122" class="Number">4</a> <a id="124" href="Agda.Builtin.Equality.html#133" class="Datatype Operator">_≡_</a>
+<a id="128" class="Keyword">data</a> <a id="_≡_"></a><a id="133" href="Agda.Builtin.Equality.html#133" class="Datatype Operator">_≡_</a> <a id="137" class="Symbol">{</a><a id="138" href="Agda.Builtin.Equality.html#138" class="Bound">a</a><a id="139" class="Symbol">}</a> <a id="141" class="Symbol">{</a><a id="142" href="Agda.Builtin.Equality.html#142" class="Bound">A</a> <a id="144" class="Symbol">:</a> <a id="146" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="150" href="Agda.Builtin.Equality.html#138" class="Bound">a</a><a id="151" class="Symbol">}</a> <a id="153" class="Symbol">(</a><a id="154" href="Agda.Builtin.Equality.html#154" class="Bound">x</a> <a id="156" class="Symbol">:</a> <a id="158" href="Agda.Builtin.Equality.html#142" class="Bound">A</a><a id="159" class="Symbol">)</a> <a id="161" class="Symbol">:</a> <a id="163" href="Agda.Builtin.Equality.html#142" class="Bound">A</a> <a id="165" class="Symbol">→</a> <a id="167" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="171" href="Agda.Builtin.Equality.html#138" class="Bound">a</a> <a id="173" class="Keyword">where</a>
+  <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>
diff --git a/docs/Agda.Builtin.Maybe.html b/docs/Agda.Builtin.Maybe.html
@@ -0,0 +1,9 @@
+<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>
+
+<a id="113" class="Keyword">data</a> <a id="Maybe"></a><a id="118" href="Agda.Builtin.Maybe.html#118" class="Datatype">Maybe</a> <a id="124" class="Symbol">{</a><a id="125" href="Agda.Builtin.Maybe.html#125" class="Bound">a</a><a id="126" class="Symbol">}</a> <a id="128" class="Symbol">(</a><a id="129" href="Agda.Builtin.Maybe.html#129" class="Bound">A</a> <a id="131" class="Symbol">:</a> <a id="133" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="137" href="Agda.Builtin.Maybe.html#125" class="Bound">a</a><a id="138" class="Symbol">)</a> <a id="140" class="Symbol">:</a> <a id="142" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="146" href="Agda.Builtin.Maybe.html#125" class="Bound">a</a> <a id="148" class="Keyword">where</a>
+  <a id="Maybe.just"></a><a id="156" href="Agda.Builtin.Maybe.html#156" class="InductiveConstructor">just</a> <a id="161" class="Symbol">:</a> <a id="163" href="Agda.Builtin.Maybe.html#129" class="Bound">A</a> <a id="165" class="Symbol">→</a> <a id="167" href="Agda.Builtin.Maybe.html#118" class="Datatype">Maybe</a> <a id="173" href="Agda.Builtin.Maybe.html#129" class="Bound">A</a>
+  <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>