-
Notifications
You must be signed in to change notification settings - Fork 0
/
Cubical.Data.Maybe.Base.html
32 lines (25 loc) · 11.6 KB
/
Cubical.Data.Maybe.Base.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Data.Maybe.Base</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">--safe</a> <a id="20" class="Symbol">#-}</a>
<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.Data.Maybe.Base.html" class="Module">Cubical.Data.Maybe.Base</a> <a id="55" class="Keyword">where</a>
<a id="62" class="Keyword">open</a> <a id="67" class="Keyword">import</a> <a id="74" href="Cubical.Core.Everything.html" class="Module">Cubical.Core.Everything</a>
<a id="99" class="Keyword">private</a>
<a id="109" class="Keyword">variable</a>
<a id="122" href="Cubical.Data.Maybe.Base.html#122" class="Generalizable">ℓ</a> <a id="124" href="Cubical.Data.Maybe.Base.html#124" class="Generalizable">ℓA</a> <a id="127" href="Cubical.Data.Maybe.Base.html#127" class="Generalizable">ℓB</a> <a id="130" class="Symbol">:</a> <a id="132" href="Agda.Primitive.html#597" class="Postulate">Level</a>
<a id="142" href="Cubical.Data.Maybe.Base.html#142" class="Generalizable">A</a> <a id="144" class="Symbol">:</a> <a id="146" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="151" href="Cubical.Data.Maybe.Base.html#124" class="Generalizable">ℓA</a>
<a id="158" href="Cubical.Data.Maybe.Base.html#158" class="Generalizable">B</a> <a id="160" class="Symbol">:</a> <a id="162" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="167" href="Cubical.Data.Maybe.Base.html#127" class="Generalizable">ℓB</a>
<a id="171" class="Keyword">data</a> <a id="Maybe"></a><a id="176" href="Cubical.Data.Maybe.Base.html#176" class="Datatype">Maybe</a> <a id="182" class="Symbol">(</a><a id="183" href="Cubical.Data.Maybe.Base.html#183" class="Bound">A</a> <a id="185" class="Symbol">:</a> <a id="187" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="192" href="Cubical.Data.Maybe.Base.html#122" class="Generalizable">ℓ</a><a id="193" class="Symbol">)</a> <a id="195" class="Symbol">:</a> <a id="197" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="202" href="Cubical.Data.Maybe.Base.html#192" class="Bound">ℓ</a> <a id="204" class="Keyword">where</a>
<a id="Maybe.nothing"></a><a id="212" href="Cubical.Data.Maybe.Base.html#212" class="InductiveConstructor">nothing</a> <a id="220" class="Symbol">:</a> <a id="222" href="Cubical.Data.Maybe.Base.html#176" class="Datatype">Maybe</a> <a id="228" href="Cubical.Data.Maybe.Base.html#183" class="Bound">A</a>
<a id="Maybe.just"></a><a id="232" href="Cubical.Data.Maybe.Base.html#232" class="InductiveConstructor">just</a> <a id="240" class="Symbol">:</a> <a id="242" href="Cubical.Data.Maybe.Base.html#183" class="Bound">A</a> <a id="244" class="Symbol">→</a> <a id="246" href="Cubical.Data.Maybe.Base.html#176" class="Datatype">Maybe</a> <a id="252" href="Cubical.Data.Maybe.Base.html#183" class="Bound">A</a>
<a id="caseMaybe"></a><a id="255" href="Cubical.Data.Maybe.Base.html#255" class="Function">caseMaybe</a> <a id="265" class="Symbol">:</a> <a id="267" class="Symbol">(</a><a id="268" href="Cubical.Data.Maybe.Base.html#268" class="Bound">n</a> <a id="270" href="Cubical.Data.Maybe.Base.html#270" class="Bound">j</a> <a id="272" class="Symbol">:</a> <a id="274" href="Cubical.Data.Maybe.Base.html#158" class="Generalizable">B</a><a id="275" class="Symbol">)</a> <a id="277" class="Symbol">→</a> <a id="279" href="Cubical.Data.Maybe.Base.html#176" class="Datatype">Maybe</a> <a id="285" href="Cubical.Data.Maybe.Base.html#142" class="Generalizable">A</a> <a id="287" class="Symbol">→</a> <a id="289" href="Cubical.Data.Maybe.Base.html#158" class="Generalizable">B</a>
<a id="291" href="Cubical.Data.Maybe.Base.html#255" class="Function">caseMaybe</a> <a id="301" href="Cubical.Data.Maybe.Base.html#301" class="Bound">n</a> <a id="303" class="Symbol">_</a> <a id="305" href="Cubical.Data.Maybe.Base.html#212" class="InductiveConstructor">nothing</a> <a id="314" class="Symbol">=</a> <a id="316" href="Cubical.Data.Maybe.Base.html#301" class="Bound">n</a>
<a id="318" href="Cubical.Data.Maybe.Base.html#255" class="Function">caseMaybe</a> <a id="328" class="Symbol">_</a> <a id="330" href="Cubical.Data.Maybe.Base.html#330" class="Bound">j</a> <a id="332" class="Symbol">(</a><a id="333" href="Cubical.Data.Maybe.Base.html#232" class="InductiveConstructor">just</a> <a id="338" class="Symbol">_)</a> <a id="341" class="Symbol">=</a> <a id="343" href="Cubical.Data.Maybe.Base.html#330" class="Bound">j</a>
<a id="map-Maybe"></a><a id="346" href="Cubical.Data.Maybe.Base.html#346" class="Function">map-Maybe</a> <a id="356" class="Symbol">:</a> <a id="358" class="Symbol">(</a><a id="359" href="Cubical.Data.Maybe.Base.html#142" class="Generalizable">A</a> <a id="361" class="Symbol">→</a> <a id="363" href="Cubical.Data.Maybe.Base.html#158" class="Generalizable">B</a><a id="364" class="Symbol">)</a> <a id="366" class="Symbol">→</a> <a id="368" href="Cubical.Data.Maybe.Base.html#176" class="Datatype">Maybe</a> <a id="374" href="Cubical.Data.Maybe.Base.html#142" class="Generalizable">A</a> <a id="376" class="Symbol">→</a> <a id="378" href="Cubical.Data.Maybe.Base.html#176" class="Datatype">Maybe</a> <a id="384" href="Cubical.Data.Maybe.Base.html#158" class="Generalizable">B</a>
<a id="386" href="Cubical.Data.Maybe.Base.html#346" class="Function">map-Maybe</a> <a id="396" class="Symbol">_</a> <a id="398" href="Cubical.Data.Maybe.Base.html#212" class="InductiveConstructor">nothing</a> <a id="407" class="Symbol">=</a> <a id="409" href="Cubical.Data.Maybe.Base.html#212" class="InductiveConstructor">nothing</a>
<a id="417" href="Cubical.Data.Maybe.Base.html#346" class="Function">map-Maybe</a> <a id="427" href="Cubical.Data.Maybe.Base.html#427" class="Bound">f</a> <a id="429" class="Symbol">(</a><a id="430" href="Cubical.Data.Maybe.Base.html#232" class="InductiveConstructor">just</a> <a id="435" href="Cubical.Data.Maybe.Base.html#435" class="Bound">x</a><a id="436" class="Symbol">)</a> <a id="438" class="Symbol">=</a> <a id="440" href="Cubical.Data.Maybe.Base.html#232" class="InductiveConstructor">just</a> <a id="445" class="Symbol">(</a><a id="446" href="Cubical.Data.Maybe.Base.html#427" class="Bound">f</a> <a id="448" href="Cubical.Data.Maybe.Base.html#435" class="Bound">x</a><a id="449" class="Symbol">)</a>
<a id="rec"></a><a id="452" href="Cubical.Data.Maybe.Base.html#452" class="Function">rec</a> <a id="456" class="Symbol">:</a> <a id="458" href="Cubical.Data.Maybe.Base.html#158" class="Generalizable">B</a> <a id="460" class="Symbol">→</a> <a id="462" class="Symbol">(</a><a id="463" href="Cubical.Data.Maybe.Base.html#142" class="Generalizable">A</a> <a id="465" class="Symbol">→</a> <a id="467" href="Cubical.Data.Maybe.Base.html#158" class="Generalizable">B</a><a id="468" class="Symbol">)</a> <a id="470" class="Symbol">→</a> <a id="472" href="Cubical.Data.Maybe.Base.html#176" class="Datatype">Maybe</a> <a id="478" href="Cubical.Data.Maybe.Base.html#142" class="Generalizable">A</a> <a id="480" class="Symbol">→</a> <a id="482" href="Cubical.Data.Maybe.Base.html#158" class="Generalizable">B</a>
<a id="484" href="Cubical.Data.Maybe.Base.html#452" class="Function">rec</a> <a id="488" href="Cubical.Data.Maybe.Base.html#488" class="Bound">n</a> <a id="490" href="Cubical.Data.Maybe.Base.html#490" class="Bound">j</a> <a id="492" href="Cubical.Data.Maybe.Base.html#212" class="InductiveConstructor">nothing</a> <a id="500" class="Symbol">=</a> <a id="502" href="Cubical.Data.Maybe.Base.html#488" class="Bound">n</a>
<a id="504" href="Cubical.Data.Maybe.Base.html#452" class="Function">rec</a> <a id="508" href="Cubical.Data.Maybe.Base.html#508" class="Bound">n</a> <a id="510" href="Cubical.Data.Maybe.Base.html#510" class="Bound">j</a> <a id="512" class="Symbol">(</a><a id="513" href="Cubical.Data.Maybe.Base.html#232" class="InductiveConstructor">just</a> <a id="518" href="Cubical.Data.Maybe.Base.html#518" class="Bound">a</a><a id="519" class="Symbol">)</a> <a id="521" class="Symbol">=</a> <a id="523" href="Cubical.Data.Maybe.Base.html#510" class="Bound">j</a> <a id="525" href="Cubical.Data.Maybe.Base.html#518" class="Bound">a</a>
<a id="elim"></a><a id="528" href="Cubical.Data.Maybe.Base.html#528" class="Function">elim</a> <a id="533" class="Symbol">:</a> <a id="535" class="Symbol">∀</a> <a id="537" class="Symbol">{</a><a id="538" href="Cubical.Data.Maybe.Base.html#538" class="Bound">A</a> <a id="540" class="Symbol">:</a> <a id="542" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="547" href="Cubical.Data.Maybe.Base.html#124" class="Generalizable">ℓA</a><a id="549" class="Symbol">}</a> <a id="551" class="Symbol">(</a><a id="552" href="Cubical.Data.Maybe.Base.html#552" class="Bound">B</a> <a id="554" class="Symbol">:</a> <a id="556" href="Cubical.Data.Maybe.Base.html#176" class="Datatype">Maybe</a> <a id="562" href="Cubical.Data.Maybe.Base.html#538" class="Bound">A</a> <a id="564" class="Symbol">→</a> <a id="566" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="571" href="Cubical.Data.Maybe.Base.html#127" class="Generalizable">ℓB</a><a id="573" class="Symbol">)</a> <a id="575" class="Symbol">→</a> <a id="577" href="Cubical.Data.Maybe.Base.html#552" class="Bound">B</a> <a id="579" href="Cubical.Data.Maybe.Base.html#212" class="InductiveConstructor">nothing</a> <a id="587" class="Symbol">→</a> <a id="589" class="Symbol">((</a><a id="591" href="Cubical.Data.Maybe.Base.html#591" class="Bound">x</a> <a id="593" class="Symbol">:</a> <a id="595" href="Cubical.Data.Maybe.Base.html#538" class="Bound">A</a><a id="596" class="Symbol">)</a> <a id="598" class="Symbol">→</a> <a id="600" href="Cubical.Data.Maybe.Base.html#552" class="Bound">B</a> <a id="602" class="Symbol">(</a><a id="603" href="Cubical.Data.Maybe.Base.html#232" class="InductiveConstructor">just</a> <a id="608" href="Cubical.Data.Maybe.Base.html#591" class="Bound">x</a><a id="609" class="Symbol">))</a> <a id="612" class="Symbol">→</a> <a id="614" class="Symbol">(</a><a id="615" href="Cubical.Data.Maybe.Base.html#615" class="Bound">mx</a> <a id="618" class="Symbol">:</a> <a id="620" href="Cubical.Data.Maybe.Base.html#176" class="Datatype">Maybe</a> <a id="626" href="Cubical.Data.Maybe.Base.html#538" class="Bound">A</a><a id="627" class="Symbol">)</a> <a id="629" class="Symbol">→</a> <a id="631" href="Cubical.Data.Maybe.Base.html#552" class="Bound">B</a> <a id="633" href="Cubical.Data.Maybe.Base.html#615" class="Bound">mx</a>
<a id="636" href="Cubical.Data.Maybe.Base.html#528" class="Function">elim</a> <a id="641" href="Cubical.Data.Maybe.Base.html#641" class="Bound">B</a> <a id="643" href="Cubical.Data.Maybe.Base.html#643" class="Bound">n</a> <a id="645" href="Cubical.Data.Maybe.Base.html#645" class="Bound">j</a> <a id="647" href="Cubical.Data.Maybe.Base.html#212" class="InductiveConstructor">nothing</a> <a id="655" class="Symbol">=</a> <a id="657" href="Cubical.Data.Maybe.Base.html#643" class="Bound">n</a>
<a id="659" href="Cubical.Data.Maybe.Base.html#528" class="Function">elim</a> <a id="664" href="Cubical.Data.Maybe.Base.html#664" class="Bound">B</a> <a id="666" href="Cubical.Data.Maybe.Base.html#666" class="Bound">n</a> <a id="668" href="Cubical.Data.Maybe.Base.html#668" class="Bound">j</a> <a id="670" class="Symbol">(</a><a id="671" href="Cubical.Data.Maybe.Base.html#232" class="InductiveConstructor">just</a> <a id="676" href="Cubical.Data.Maybe.Base.html#676" class="Bound">a</a><a id="677" class="Symbol">)</a> <a id="679" class="Symbol">=</a> <a id="681" href="Cubical.Data.Maybe.Base.html#668" class="Bound">j</a> <a id="683" href="Cubical.Data.Maybe.Base.html#676" class="Bound">a</a>
</pre></body></html>