-
Notifications
You must be signed in to change notification settings - Fork 0
/
Agda.Builtin.List.html
19 lines (15 loc) · 4.69 KB
/
Agda.Builtin.List.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
<!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>
<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>
<a id="130" class="Keyword">infixr</a> <a id="137" class="Number">5</a> <a id="139" href="Agda.Builtin.List.html#200" class="InductiveConstructor Operator">_∷_</a>
<a id="143" class="Keyword">data</a> <a id="List"></a><a id="148" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="153" class="Symbol">{</a><a id="154" href="Agda.Builtin.List.html#154" class="Bound">a</a><a id="155" class="Symbol">}</a> <a id="157" class="Symbol">(</a><a id="158" href="Agda.Builtin.List.html#158" class="Bound">A</a> <a id="160" class="Symbol">:</a> <a id="162" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="166" href="Agda.Builtin.List.html#154" class="Bound">a</a><a id="167" class="Symbol">)</a> <a id="169" class="Symbol">:</a> <a id="171" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="175" href="Agda.Builtin.List.html#154" class="Bound">a</a> <a id="177" class="Keyword">where</a>
<a id="List.[]"></a><a id="185" href="Agda.Builtin.List.html#185" class="InductiveConstructor">[]</a> <a id="189" class="Symbol">:</a> <a id="191" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="196" href="Agda.Builtin.List.html#158" class="Bound">A</a>
<a id="List._∷_"></a><a id="200" href="Agda.Builtin.List.html#200" class="InductiveConstructor Operator">_∷_</a> <a id="204" class="Symbol">:</a> <a id="206" class="Symbol">(</a><a id="207" href="Agda.Builtin.List.html#207" class="Bound">x</a> <a id="209" class="Symbol">:</a> <a id="211" href="Agda.Builtin.List.html#158" class="Bound">A</a><a id="212" class="Symbol">)</a> <a id="214" class="Symbol">(</a><a id="215" href="Agda.Builtin.List.html#215" class="Bound">xs</a> <a id="218" class="Symbol">:</a> <a id="220" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="225" href="Agda.Builtin.List.html#158" class="Bound">A</a><a id="226" class="Symbol">)</a> <a id="228" class="Symbol">→</a> <a id="230" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="235" href="Agda.Builtin.List.html#158" class="Bound">A</a>
<a id="238" class="Symbol">{-#</a> <a id="242" class="Keyword">BUILTIN</a> <a id="250" class="Keyword">LIST</a> <a id="255" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="260" class="Symbol">#-}</a>
<a id="265" class="Symbol">{-#</a> <a id="269" class="Keyword">COMPILE</a> <a id="277" class="Keyword">JS</a> <a id="281" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="286" class="Pragma">=</a> <a id="288" class="Pragma">function(x,v)</a> <a id="302" class="Pragma">{</a>
<a id="306" class="Pragma">if</a> <a id="309" class="Pragma">(x.length</a> <a id="319" class="Pragma"><</a> <a id="321" class="Pragma">1)</a> <a id="324" class="Pragma">{</a> <a id="326" class="Pragma">return</a> <a id="333" class="Pragma">v["[]"]();</a> <a id="344" class="Pragma">}</a> <a id="346" class="Pragma">else</a> <a id="351" class="Pragma">{</a> <a id="353" class="Pragma">return</a> <a id="360" class="Pragma">v["_∷_"](x[0],</a> <a id="375" class="Pragma">x.slice(1));</a> <a id="388" class="Pragma">}</a>
<a id="390" class="Pragma">}</a> <a id="392" class="Symbol">#-}</a>
<a id="396" class="Symbol">{-#</a> <a id="400" class="Keyword">COMPILE</a> <a id="408" class="Keyword">JS</a> <a id="411" href="Agda.Builtin.List.html#185" class="InductiveConstructor">[]</a> <a id="414" class="Pragma">=</a> <a id="416" class="Pragma">Array()</a> <a id="424" class="Symbol">#-}</a>
<a id="428" class="Symbol">{-#</a> <a id="432" class="Keyword">COMPILE</a> <a id="440" class="Keyword">JS</a> <a id="443" href="Agda.Builtin.List.html#200" class="InductiveConstructor Operator">_∷_</a> <a id="447" class="Pragma">=</a> <a id="449" class="Pragma">function</a> <a id="458" class="Pragma">(x)</a> <a id="462" class="Pragma">{</a> <a id="464" class="Pragma">return</a> <a id="471" class="Pragma">function(y)</a> <a id="483" class="Pragma">{</a> <a id="485" class="Pragma">return</a> <a id="492" class="Pragma">Array(x).concat(y);</a> <a id="512" class="Pragma">};</a> <a id="515" class="Pragma">}</a> <a id="517" class="Symbol">#-}</a>
</pre></body></html>