Skip to content

Commit 75f8242

Browse files
omelkonianomelkonian
committed
deploy: 7136569 
0 parents  commit 75f8242

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

81 files changed

+12132
-0
lines changed

‎.nojekyll‎

Whitespace-only changes.

‎Agda.Builtin.Bool.html‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
<!DOCTYPE HTML>
2+
<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>
3+
<a id="80" class="Pragma">--no-sized-types</a> <a id="97" class="Pragma">--no-guardedness</a> <a id="114" class="Pragma">--level-universe</a> <a id="131" class="Symbol">#-}</a>
4+
5+
<a id="136" class="Keyword">module</a> <a id="143" href="Agda.Builtin.Bool.html" class="Module">Agda.Builtin.Bool</a> <a id="161" class="Keyword">where</a>
6+
7+
<a id="168" class="Keyword">data</a> <a id="Bool"></a><a id="173" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="178" class="Symbol">:</a> <a id="180" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="184" class="Keyword">where</a>
8+
<a id="Bool.false"></a><a id="192" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="Bool.true"></a><a id="198" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="203" class="Symbol">:</a> <a id="205" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a>
9+
10+
<a id="211" class="Symbol">{-#</a> <a id="215" class="Keyword">BUILTIN</a> <a id="223" class="Keyword">BOOL</a> <a id="229" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="235" class="Symbol">#-}</a>
11+
<a id="239" class="Symbol">{-#</a> <a id="243" class="Keyword">BUILTIN</a> <a id="251" class="Keyword">FALSE</a> <a id="257" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="263" class="Symbol">#-}</a>
12+
<a id="267" class="Symbol">{-#</a> <a id="271" class="Keyword">BUILTIN</a> <a id="279" class="Keyword">TRUE</a> <a id="285" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="291" class="Symbol">#-}</a>
13+
14+
<a id="296" class="Symbol">{-#</a> <a id="300" class="Keyword">COMPILE</a> <a id="308" class="Keyword">JS</a> <a id="311" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="317" class="Pragma">=</a> <a id="319" class="Pragma">function</a> <a id="328" class="Pragma">(x,v)</a> <a id="334" class="Pragma">{</a> <a id="336" class="Pragma">return</a> <a id="343" class="Pragma">((x)?</a> <a id="349" class="Pragma">v[&quot;true&quot;]()</a> <a id="361" class="Pragma">:</a> <a id="363" class="Pragma">v[&quot;false&quot;]());</a> <a id="378" class="Pragma">}</a> <a id="380" class="Symbol">#-}</a>
15+
<a id="384" class="Symbol">{-#</a> <a id="388" class="Keyword">COMPILE</a> <a id="396" class="Keyword">JS</a> <a id="399" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="405" class="Pragma">=</a> <a id="407" class="Pragma">false</a> <a id="413" class="Symbol">#-}</a>
16+
<a id="417" class="Symbol">{-#</a> <a id="421" class="Keyword">COMPILE</a> <a id="429" class="Keyword">JS</a> <a id="432" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="438" class="Pragma">=</a> <a id="440" class="Pragma">true</a> <a id="446" class="Symbol">#-}</a>
17+
</pre></body></html>

‎Agda.Builtin.Equality.html‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
<!DOCTYPE HTML>
2+
<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="Pragma">--level-universe</a> <a id="92" class="Symbol">#-}</a>
3+
4+
<a id="97" class="Keyword">module</a> <a id="104" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a> <a id="126" class="Keyword">where</a>
5+
6+
<a id="133" class="Keyword">infix</a> <a id="139" class="Number">4</a> <a id="141" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">_≡_</a>
7+
<a id="145" class="Keyword">data</a> <a id="_≡_"></a><a id="150" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">_≡_</a> <a id="154" class="Symbol">{</a><a id="155" href="Agda.Builtin.Equality.html#155" class="Bound">a</a><a id="156" class="Symbol">}</a> <a id="158" class="Symbol">{</a><a id="159" href="Agda.Builtin.Equality.html#159" class="Bound">A</a> <a id="161" class="Symbol">:</a> <a id="163" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="167" href="Agda.Builtin.Equality.html#155" class="Bound">a</a><a id="168" class="Symbol">}</a> <a id="170" class="Symbol">(</a><a id="171" href="Agda.Builtin.Equality.html#171" class="Bound">x</a> <a id="173" class="Symbol">:</a> <a id="175" href="Agda.Builtin.Equality.html#159" class="Bound">A</a><a id="176" class="Symbol">)</a> <a id="178" class="Symbol">:</a> <a id="180" href="Agda.Builtin.Equality.html#159" class="Bound">A</a> <a id="182" class="Symbol">→</a> <a id="184" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="188" href="Agda.Builtin.Equality.html#155" class="Bound">a</a> <a id="190" class="Keyword">where</a>
8+
<a id="198" class="Keyword">instance</a> <a id="_≡_.refl"></a><a id="207" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> <a id="212" class="Symbol">:</a> <a id="214" href="Agda.Builtin.Equality.html#171" class="Bound">x</a> <a id="216" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="218" href="Agda.Builtin.Equality.html#171" class="Bound">x</a>
9+
10+
<a id="221" class="Symbol">{-#</a> <a id="225" class="Keyword">BUILTIN</a> <a id="233" class="Keyword">EQUALITY</a> <a id="242" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">_≡_</a> <a id="246" class="Symbol">#-}</a>
11+
</pre></body></html>

‎Agda.Builtin.List.html‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
<!DOCTYPE HTML>
2+
<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">--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="Pragma">--level-universe</a> <a id="92" class="Symbol">#-}</a>
3+
4+
<a id="97" class="Keyword">module</a> <a id="104" href="Agda.Builtin.List.html" class="Module">Agda.Builtin.List</a> <a id="122" class="Keyword">where</a>
5+
6+
<a id="129" class="Keyword">infixr</a> <a id="136" class="Number">5</a> <a id="138" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">_∷_</a>
7+
<a id="142" class="Keyword">data</a> <a id="List"></a><a id="147" href="Agda.Builtin.List.html#147" class="Datatype">List</a> <a id="152" class="Symbol">{</a><a id="153" href="Agda.Builtin.List.html#153" class="Bound">a</a><a id="154" class="Symbol">}</a> <a id="156" class="Symbol">(</a><a id="157" href="Agda.Builtin.List.html#157" class="Bound">A</a> <a id="159" class="Symbol">:</a> <a id="161" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="165" href="Agda.Builtin.List.html#153" class="Bound">a</a><a id="166" class="Symbol">)</a> <a id="168" class="Symbol">:</a> <a id="170" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="174" href="Agda.Builtin.List.html#153" class="Bound">a</a> <a id="176" class="Keyword">where</a>
8+
<a id="List.[]"></a><a id="184" href="Agda.Builtin.List.html#184" class="InductiveConstructor">[]</a> <a id="188" class="Symbol">:</a> <a id="190" href="Agda.Builtin.List.html#147" class="Datatype">List</a> <a id="195" href="Agda.Builtin.List.html#157" class="Bound">A</a>
9+
<a id="List._∷_"></a><a id="199" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">_∷_</a> <a id="203" class="Symbol">:</a> <a id="205" class="Symbol">(</a><a id="206" href="Agda.Builtin.List.html#206" class="Bound">x</a> <a id="208" class="Symbol">:</a> <a id="210" href="Agda.Builtin.List.html#157" class="Bound">A</a><a id="211" class="Symbol">)</a> <a id="213" class="Symbol">(</a><a id="214" href="Agda.Builtin.List.html#214" class="Bound">xs</a> <a id="217" class="Symbol">:</a> <a id="219" href="Agda.Builtin.List.html#147" class="Datatype">List</a> <a id="224" href="Agda.Builtin.List.html#157" class="Bound">A</a><a id="225" class="Symbol">)</a> <a id="227" class="Symbol">→</a> <a id="229" href="Agda.Builtin.List.html#147" class="Datatype">List</a> <a id="234" href="Agda.Builtin.List.html#157" class="Bound">A</a>
10+
11+
<a id="237" class="Symbol">{-#</a> <a id="241" class="Keyword">BUILTIN</a> <a id="249" class="Keyword">LIST</a> <a id="254" href="Agda.Builtin.List.html#147" class="Datatype">List</a> <a id="259" class="Symbol">#-}</a>
12+
13+
<a id="264" class="Symbol">{-#</a> <a id="268" class="Keyword">COMPILE</a> <a id="276" class="Keyword">JS</a> <a id="280" href="Agda.Builtin.List.html#147" class="Datatype">List</a> <a id="285" class="Pragma">=</a> <a id="287" class="Pragma">function(x,v)</a> <a id="301" class="Pragma">{</a>
14+
<a id="305" class="Pragma">if</a> <a id="308" class="Pragma">(x.length</a> <a id="318" class="Pragma">&lt;</a> <a id="320" class="Pragma">1)</a> <a id="323" class="Pragma">{</a> <a id="325" class="Pragma">return</a> <a id="332" class="Pragma">v[&quot;[]&quot;]();</a> <a id="343" class="Pragma">}</a> <a id="345" class="Pragma">else</a> <a id="350" class="Pragma">{</a> <a id="352" class="Pragma">return</a> <a id="359" class="Pragma">v[&quot;_∷_&quot;](x[0],</a> <a id="374" class="Pragma">x.slice(1));</a> <a id="387" class="Pragma">}</a>
15+
<a id="389" class="Pragma">}</a> <a id="391" class="Symbol">#-}</a>
16+
<a id="395" class="Symbol">{-#</a> <a id="399" class="Keyword">COMPILE</a> <a id="407" class="Keyword">JS</a> <a id="410" href="Agda.Builtin.List.html#184" class="InductiveConstructor">[]</a> <a id="413" class="Pragma">=</a> <a id="415" class="Pragma">Array()</a> <a id="423" class="Symbol">#-}</a>
17+
<a id="427" class="Symbol">{-#</a> <a id="431" class="Keyword">COMPILE</a> <a id="439" class="Keyword">JS</a> <a id="442" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">_∷_</a> <a id="446" class="Pragma">=</a> <a id="448" class="Pragma">function</a> <a id="457" class="Pragma">(x)</a> <a id="461" class="Pragma">{</a> <a id="463" class="Pragma">return</a> <a id="470" class="Pragma">function(y)</a> <a id="482" class="Pragma">{</a> <a id="484" class="Pragma">return</a> <a id="491" class="Pragma">Array(x).concat(y);</a> <a id="511" class="Pragma">};</a> <a id="514" class="Pragma">}</a> <a id="516" class="Symbol">#-}</a>
18+
</pre></body></html>

0 commit comments

Comments
 (0)