82 lines
36 KiB
HTML
82 lines
36 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Data.These.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">-- An either-or-both data type, basic type and operations</a>
|
||
<a id="164" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="238" class="Symbol">{-#</a> <a id="242" class="Keyword">OPTIONS</a> <a id="250" class="Pragma">--without-K</a> <a id="262" class="Pragma">--safe</a> <a id="269" class="Symbol">#-}</a>
|
||
|
||
<a id="274" class="Keyword">module</a> <a id="281" href="Data.These.Base.html" class="Module">Data.These.Base</a> <a id="297" class="Keyword">where</a>
|
||
|
||
<a id="304" class="Keyword">open</a> <a id="309" class="Keyword">import</a> <a id="316" href="Level.html" class="Module">Level</a>
|
||
<a id="322" class="Keyword">open</a> <a id="327" class="Keyword">import</a> <a id="334" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a> <a id="348" class="Keyword">using</a> <a id="354" class="Symbol">(</a><a id="355" href="Data.Sum.Base.html#734" class="Datatype Operator">_⊎_</a><a id="358" class="Symbol">;</a> <a id="360" href="Data.Sum.Base.html#1089" class="Function Operator">[_,_]′</a><a id="366" class="Symbol">)</a>
|
||
<a id="368" class="Keyword">open</a> <a id="373" class="Keyword">import</a> <a id="380" href="Function.Base.html" class="Module">Function.Base</a>
|
||
|
||
<a id="395" class="Keyword">private</a>
|
||
<a id="405" class="Keyword">variable</a>
|
||
<a id="418" href="Data.These.Base.html#418" class="Generalizable">a</a> <a id="420" href="Data.These.Base.html#420" class="Generalizable">b</a> <a id="422" href="Data.These.Base.html#422" class="Generalizable">c</a> <a id="424" href="Data.These.Base.html#424" class="Generalizable">d</a> <a id="426" href="Data.These.Base.html#426" class="Generalizable">e</a> <a id="428" href="Data.These.Base.html#428" class="Generalizable">f</a> <a id="430" class="Symbol">:</a> <a id="432" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="442" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="444" class="Symbol">:</a> <a id="446" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="450" href="Data.These.Base.html#418" class="Generalizable">a</a>
|
||
<a id="456" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="458" class="Symbol">:</a> <a id="460" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="464" href="Data.These.Base.html#420" class="Generalizable">b</a>
|
||
<a id="470" href="Data.These.Base.html#470" class="Generalizable">C</a> <a id="472" class="Symbol">:</a> <a id="474" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="478" href="Data.These.Base.html#422" class="Generalizable">c</a>
|
||
<a id="484" href="Data.These.Base.html#484" class="Generalizable">D</a> <a id="486" class="Symbol">:</a> <a id="488" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="492" href="Data.These.Base.html#424" class="Generalizable">d</a>
|
||
<a id="498" href="Data.These.Base.html#498" class="Generalizable">E</a> <a id="500" class="Symbol">:</a> <a id="502" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="506" href="Data.These.Base.html#426" class="Generalizable">e</a>
|
||
<a id="512" href="Data.These.Base.html#512" class="Generalizable">F</a> <a id="514" class="Symbol">:</a> <a id="516" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="520" href="Data.These.Base.html#428" class="Generalizable">f</a>
|
||
|
||
<a id="523" class="Keyword">data</a> <a id="These"></a><a id="528" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="534" class="Symbol">{</a><a id="535" href="Data.These.Base.html#535" class="Bound">a</a> <a id="537" href="Data.These.Base.html#537" class="Bound">b</a><a id="538" class="Symbol">}</a> <a id="540" class="Symbol">(</a><a id="541" href="Data.These.Base.html#541" class="Bound">A</a> <a id="543" class="Symbol">:</a> <a id="545" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="549" href="Data.These.Base.html#535" class="Bound">a</a><a id="550" class="Symbol">)</a> <a id="552" class="Symbol">(</a><a id="553" href="Data.These.Base.html#553" class="Bound">B</a> <a id="555" class="Symbol">:</a> <a id="557" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="561" href="Data.These.Base.html#537" class="Bound">b</a><a id="562" class="Symbol">)</a> <a id="564" class="Symbol">:</a> <a id="566" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="570" class="Symbol">(</a><a id="571" href="Data.These.Base.html#535" class="Bound">a</a> <a id="573" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="575" href="Data.These.Base.html#537" class="Bound">b</a><a id="576" class="Symbol">)</a> <a id="578" class="Keyword">where</a>
|
||
<a id="These.this"></a><a id="586" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="592" class="Symbol">:</a> <a id="594" href="Data.These.Base.html#541" class="Bound">A</a> <a id="600" class="Symbol">→</a> <a id="602" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="608" href="Data.These.Base.html#541" class="Bound">A</a> <a id="610" href="Data.These.Base.html#553" class="Bound">B</a>
|
||
<a id="These.that"></a><a id="614" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="620" class="Symbol">:</a> <a id="626" href="Data.These.Base.html#553" class="Bound">B</a> <a id="628" class="Symbol">→</a> <a id="630" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="636" href="Data.These.Base.html#541" class="Bound">A</a> <a id="638" href="Data.These.Base.html#553" class="Bound">B</a>
|
||
<a id="These.these"></a><a id="642" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="648" class="Symbol">:</a> <a id="650" href="Data.These.Base.html#541" class="Bound">A</a> <a id="652" class="Symbol">→</a> <a id="654" href="Data.These.Base.html#553" class="Bound">B</a> <a id="656" class="Symbol">→</a> <a id="658" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="664" href="Data.These.Base.html#541" class="Bound">A</a> <a id="666" href="Data.These.Base.html#553" class="Bound">B</a>
|
||
|
||
<a id="669" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="742" class="Comment">-- Operations</a>
|
||
|
||
<a id="757" class="Comment">-- injection</a>
|
||
|
||
<a id="fromSum"></a><a id="771" href="Data.These.Base.html#771" class="Function">fromSum</a> <a id="779" class="Symbol">:</a> <a id="781" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="783" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="785" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="787" class="Symbol">→</a> <a id="789" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="795" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="797" href="Data.These.Base.html#456" class="Generalizable">B</a>
|
||
<a id="799" href="Data.These.Base.html#771" class="Function">fromSum</a> <a id="807" class="Symbol">=</a> <a id="809" href="Data.Sum.Base.html#1089" class="Function Operator">[</a> <a id="811" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="816" href="Data.Sum.Base.html#1089" class="Function Operator">,</a> <a id="818" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="823" href="Data.Sum.Base.html#1089" class="Function Operator">]′</a>
|
||
|
||
<a id="827" class="Comment">-- map</a>
|
||
|
||
<a id="map"></a><a id="835" href="Data.These.Base.html#835" class="Function">map</a> <a id="839" class="Symbol">:</a> <a id="841" class="Symbol">(</a><a id="842" href="Data.These.Base.html#842" class="Bound">f</a> <a id="844" class="Symbol">:</a> <a id="846" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="848" class="Symbol">→</a> <a id="850" href="Data.These.Base.html#456" class="Generalizable">B</a><a id="851" class="Symbol">)</a> <a id="853" class="Symbol">(</a><a id="854" href="Data.These.Base.html#854" class="Bound">g</a> <a id="856" class="Symbol">:</a> <a id="858" href="Data.These.Base.html#470" class="Generalizable">C</a> <a id="860" class="Symbol">→</a> <a id="862" href="Data.These.Base.html#484" class="Generalizable">D</a><a id="863" class="Symbol">)</a> <a id="865" class="Symbol">→</a> <a id="867" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="873" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="875" href="Data.These.Base.html#470" class="Generalizable">C</a> <a id="877" class="Symbol">→</a> <a id="879" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="885" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="887" href="Data.These.Base.html#484" class="Generalizable">D</a>
|
||
<a id="889" href="Data.These.Base.html#835" class="Function">map</a> <a id="893" href="Data.These.Base.html#893" class="Bound">f</a> <a id="895" href="Data.These.Base.html#895" class="Bound">g</a> <a id="897" class="Symbol">(</a><a id="898" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="903" href="Data.These.Base.html#903" class="Bound">a</a><a id="904" class="Symbol">)</a> <a id="909" class="Symbol">=</a> <a id="911" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="916" class="Symbol">(</a><a id="917" href="Data.These.Base.html#893" class="Bound">f</a> <a id="919" href="Data.These.Base.html#903" class="Bound">a</a><a id="920" class="Symbol">)</a>
|
||
<a id="922" href="Data.These.Base.html#835" class="Function">map</a> <a id="926" href="Data.These.Base.html#926" class="Bound">f</a> <a id="928" href="Data.These.Base.html#928" class="Bound">g</a> <a id="930" class="Symbol">(</a><a id="931" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="936" href="Data.These.Base.html#936" class="Bound">b</a><a id="937" class="Symbol">)</a> <a id="942" class="Symbol">=</a> <a id="944" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="949" class="Symbol">(</a><a id="950" href="Data.These.Base.html#928" class="Bound">g</a> <a id="952" href="Data.These.Base.html#936" class="Bound">b</a><a id="953" class="Symbol">)</a>
|
||
<a id="955" href="Data.These.Base.html#835" class="Function">map</a> <a id="959" href="Data.These.Base.html#959" class="Bound">f</a> <a id="961" href="Data.These.Base.html#961" class="Bound">g</a> <a id="963" class="Symbol">(</a><a id="964" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="970" href="Data.These.Base.html#970" class="Bound">a</a> <a id="972" href="Data.These.Base.html#972" class="Bound">b</a><a id="973" class="Symbol">)</a> <a id="975" class="Symbol">=</a> <a id="977" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="983" class="Symbol">(</a><a id="984" href="Data.These.Base.html#959" class="Bound">f</a> <a id="986" href="Data.These.Base.html#970" class="Bound">a</a><a id="987" class="Symbol">)</a> <a id="989" class="Symbol">(</a><a id="990" href="Data.These.Base.html#961" class="Bound">g</a> <a id="992" href="Data.These.Base.html#972" class="Bound">b</a><a id="993" class="Symbol">)</a>
|
||
|
||
<a id="map₁"></a><a id="996" href="Data.These.Base.html#996" class="Function">map₁</a> <a id="1001" class="Symbol">:</a> <a id="1003" class="Symbol">(</a><a id="1004" href="Data.These.Base.html#1004" class="Bound">f</a> <a id="1006" class="Symbol">:</a> <a id="1008" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1010" class="Symbol">→</a> <a id="1012" href="Data.These.Base.html#456" class="Generalizable">B</a><a id="1013" class="Symbol">)</a> <a id="1015" class="Symbol">→</a> <a id="1017" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1023" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1025" href="Data.These.Base.html#470" class="Generalizable">C</a> <a id="1027" class="Symbol">→</a> <a id="1029" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1035" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1037" href="Data.These.Base.html#470" class="Generalizable">C</a>
|
||
<a id="1039" href="Data.These.Base.html#996" class="Function">map₁</a> <a id="1044" href="Data.These.Base.html#1044" class="Bound">f</a> <a id="1046" class="Symbol">=</a> <a id="1048" href="Data.These.Base.html#835" class="Function">map</a> <a id="1052" href="Data.These.Base.html#1044" class="Bound">f</a> <a id="1054" href="Function.Base.html#615" class="Function">id</a>
|
||
|
||
<a id="map₂"></a><a id="1058" href="Data.These.Base.html#1058" class="Function">map₂</a> <a id="1063" class="Symbol">:</a> <a id="1065" class="Symbol">(</a><a id="1066" href="Data.These.Base.html#1066" class="Bound">g</a> <a id="1068" class="Symbol">:</a> <a id="1070" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1072" class="Symbol">→</a> <a id="1074" href="Data.These.Base.html#470" class="Generalizable">C</a><a id="1075" class="Symbol">)</a> <a id="1077" class="Symbol">→</a> <a id="1079" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1085" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1087" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1089" class="Symbol">→</a> <a id="1091" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1097" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1099" href="Data.These.Base.html#470" class="Generalizable">C</a>
|
||
<a id="1101" href="Data.These.Base.html#1058" class="Function">map₂</a> <a id="1106" class="Symbol">=</a> <a id="1108" href="Data.These.Base.html#835" class="Function">map</a> <a id="1112" href="Function.Base.html#615" class="Function">id</a>
|
||
|
||
<a id="1116" class="Comment">-- fold</a>
|
||
|
||
<a id="fold"></a><a id="1125" href="Data.These.Base.html#1125" class="Function">fold</a> <a id="1130" class="Symbol">:</a> <a id="1132" class="Symbol">(</a><a id="1133" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1135" class="Symbol">→</a> <a id="1137" href="Data.These.Base.html#470" class="Generalizable">C</a><a id="1138" class="Symbol">)</a> <a id="1140" class="Symbol">→</a> <a id="1142" class="Symbol">(</a><a id="1143" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1145" class="Symbol">→</a> <a id="1147" href="Data.These.Base.html#470" class="Generalizable">C</a><a id="1148" class="Symbol">)</a> <a id="1150" class="Symbol">→</a> <a id="1152" class="Symbol">(</a><a id="1153" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1155" class="Symbol">→</a> <a id="1157" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1159" class="Symbol">→</a> <a id="1161" href="Data.These.Base.html#470" class="Generalizable">C</a><a id="1162" class="Symbol">)</a> <a id="1164" class="Symbol">→</a> <a id="1166" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1172" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1174" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1176" class="Symbol">→</a> <a id="1178" href="Data.These.Base.html#470" class="Generalizable">C</a>
|
||
<a id="1180" href="Data.These.Base.html#1125" class="Function">fold</a> <a id="1185" href="Data.These.Base.html#1185" class="Bound">l</a> <a id="1187" href="Data.These.Base.html#1187" class="Bound">r</a> <a id="1189" href="Data.These.Base.html#1189" class="Bound">lr</a> <a id="1192" class="Symbol">(</a><a id="1193" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="1198" href="Data.These.Base.html#1198" class="Bound">a</a><a id="1199" class="Symbol">)</a> <a id="1204" class="Symbol">=</a> <a id="1206" href="Data.These.Base.html#1185" class="Bound">l</a> <a id="1208" href="Data.These.Base.html#1198" class="Bound">a</a>
|
||
<a id="1210" href="Data.These.Base.html#1125" class="Function">fold</a> <a id="1215" href="Data.These.Base.html#1215" class="Bound">l</a> <a id="1217" href="Data.These.Base.html#1217" class="Bound">r</a> <a id="1219" href="Data.These.Base.html#1219" class="Bound">lr</a> <a id="1222" class="Symbol">(</a><a id="1223" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1228" href="Data.These.Base.html#1228" class="Bound">b</a><a id="1229" class="Symbol">)</a> <a id="1234" class="Symbol">=</a> <a id="1236" href="Data.These.Base.html#1217" class="Bound">r</a> <a id="1238" href="Data.These.Base.html#1228" class="Bound">b</a>
|
||
<a id="1240" href="Data.These.Base.html#1125" class="Function">fold</a> <a id="1245" href="Data.These.Base.html#1245" class="Bound">l</a> <a id="1247" href="Data.These.Base.html#1247" class="Bound">r</a> <a id="1249" href="Data.These.Base.html#1249" class="Bound">lr</a> <a id="1252" class="Symbol">(</a><a id="1253" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1259" href="Data.These.Base.html#1259" class="Bound">a</a> <a id="1261" href="Data.These.Base.html#1261" class="Bound">b</a><a id="1262" class="Symbol">)</a> <a id="1264" class="Symbol">=</a> <a id="1266" href="Data.These.Base.html#1249" class="Bound">lr</a> <a id="1269" href="Data.These.Base.html#1259" class="Bound">a</a> <a id="1271" href="Data.These.Base.html#1261" class="Bound">b</a>
|
||
|
||
<a id="foldWithDefaults"></a><a id="1274" href="Data.These.Base.html#1274" class="Function">foldWithDefaults</a> <a id="1291" class="Symbol">:</a> <a id="1293" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1295" class="Symbol">→</a> <a id="1297" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1299" class="Symbol">→</a> <a id="1301" class="Symbol">(</a><a id="1302" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1304" class="Symbol">→</a> <a id="1306" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1308" class="Symbol">→</a> <a id="1310" href="Data.These.Base.html#470" class="Generalizable">C</a><a id="1311" class="Symbol">)</a> <a id="1313" class="Symbol">→</a> <a id="1315" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1321" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1323" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1325" class="Symbol">→</a> <a id="1327" href="Data.These.Base.html#470" class="Generalizable">C</a>
|
||
<a id="1329" href="Data.These.Base.html#1274" class="Function">foldWithDefaults</a> <a id="1346" href="Data.These.Base.html#1346" class="Bound">a</a> <a id="1348" href="Data.These.Base.html#1348" class="Bound">b</a> <a id="1350" href="Data.These.Base.html#1350" class="Bound">lr</a> <a id="1353" class="Symbol">=</a> <a id="1355" href="Data.These.Base.html#1125" class="Function">fold</a> <a id="1360" class="Symbol">(</a><a id="1361" href="Function.Base.html#1554" class="Function">flip</a> <a id="1366" href="Data.These.Base.html#1350" class="Bound">lr</a> <a id="1369" href="Data.These.Base.html#1348" class="Bound">b</a><a id="1370" class="Symbol">)</a> <a id="1372" class="Symbol">(</a><a id="1373" href="Data.These.Base.html#1350" class="Bound">lr</a> <a id="1376" href="Data.These.Base.html#1346" class="Bound">a</a><a id="1377" class="Symbol">)</a> <a id="1379" href="Data.These.Base.html#1350" class="Bound">lr</a>
|
||
|
||
<a id="1383" class="Comment">-- swap</a>
|
||
|
||
<a id="swap"></a><a id="1392" href="Data.These.Base.html#1392" class="Function">swap</a> <a id="1397" class="Symbol">:</a> <a id="1399" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1405" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1407" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1409" class="Symbol">→</a> <a id="1411" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1417" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1419" href="Data.These.Base.html#442" class="Generalizable">A</a>
|
||
<a id="1421" href="Data.These.Base.html#1392" class="Function">swap</a> <a id="1426" class="Symbol">=</a> <a id="1428" href="Data.These.Base.html#1125" class="Function">fold</a> <a id="1433" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1438" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="1443" class="Symbol">(</a><a id="1444" href="Function.Base.html#1554" class="Function">flip</a> <a id="1449" href="Data.These.Base.html#642" class="InductiveConstructor">these</a><a id="1454" class="Symbol">)</a>
|
||
|
||
<a id="1457" class="Comment">-- align</a>
|
||
|
||
<a id="alignWith"></a><a id="1467" href="Data.These.Base.html#1467" class="Function">alignWith</a> <a id="1477" class="Symbol">:</a> <a id="1479" class="Symbol">(</a><a id="1480" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1486" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1488" href="Data.These.Base.html#470" class="Generalizable">C</a> <a id="1490" class="Symbol">→</a> <a id="1492" href="Data.These.Base.html#498" class="Generalizable">E</a><a id="1493" class="Symbol">)</a> <a id="1495" class="Symbol">→</a> <a id="1497" class="Symbol">(</a><a id="1498" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1504" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1506" href="Data.These.Base.html#484" class="Generalizable">D</a> <a id="1508" class="Symbol">→</a> <a id="1510" href="Data.These.Base.html#512" class="Generalizable">F</a><a id="1511" class="Symbol">)</a> <a id="1513" class="Symbol">→</a> <a id="1515" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1521" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="1523" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="1525" class="Symbol">→</a> <a id="1527" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1533" href="Data.These.Base.html#470" class="Generalizable">C</a> <a id="1535" href="Data.These.Base.html#484" class="Generalizable">D</a> <a id="1537" class="Symbol">→</a> <a id="1539" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="1545" href="Data.These.Base.html#498" class="Generalizable">E</a> <a id="1547" href="Data.These.Base.html#512" class="Generalizable">F</a>
|
||
<a id="1549" href="Data.These.Base.html#1467" class="Function">alignWith</a> <a id="1559" href="Data.These.Base.html#1559" class="Bound">f</a> <a id="1561" href="Data.These.Base.html#1561" class="Bound">g</a> <a id="1563" class="Symbol">(</a><a id="1564" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="1569" href="Data.These.Base.html#1569" class="Bound">a</a><a id="1570" class="Symbol">)</a> <a id="1575" class="Symbol">(</a><a id="1576" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="1581" href="Data.These.Base.html#1581" class="Bound">c</a><a id="1582" class="Symbol">)</a> <a id="1587" class="Symbol">=</a> <a id="1589" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="1594" class="Symbol">(</a><a id="1595" href="Data.These.Base.html#1559" class="Bound">f</a> <a id="1597" class="Symbol">(</a><a id="1598" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1604" href="Data.These.Base.html#1569" class="Bound">a</a> <a id="1606" href="Data.These.Base.html#1581" class="Bound">c</a><a id="1607" class="Symbol">))</a>
|
||
<a id="1610" href="Data.These.Base.html#1467" class="Function">alignWith</a> <a id="1620" href="Data.These.Base.html#1620" class="Bound">f</a> <a id="1622" href="Data.These.Base.html#1622" class="Bound">g</a> <a id="1624" class="Symbol">(</a><a id="1625" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="1630" href="Data.These.Base.html#1630" class="Bound">a</a><a id="1631" class="Symbol">)</a> <a id="1636" class="Symbol">(</a><a id="1637" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1642" href="Data.These.Base.html#1642" class="Bound">d</a><a id="1643" class="Symbol">)</a> <a id="1648" class="Symbol">=</a> <a id="1650" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1656" class="Symbol">(</a><a id="1657" href="Data.These.Base.html#1620" class="Bound">f</a> <a id="1659" class="Symbol">(</a><a id="1660" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="1665" href="Data.These.Base.html#1630" class="Bound">a</a><a id="1666" class="Symbol">))</a> <a id="1669" class="Symbol">(</a><a id="1670" href="Data.These.Base.html#1622" class="Bound">g</a> <a id="1672" class="Symbol">(</a><a id="1673" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1678" href="Data.These.Base.html#1642" class="Bound">d</a><a id="1679" class="Symbol">))</a>
|
||
<a id="1682" href="Data.These.Base.html#1467" class="Function">alignWith</a> <a id="1692" href="Data.These.Base.html#1692" class="Bound">f</a> <a id="1694" href="Data.These.Base.html#1694" class="Bound">g</a> <a id="1696" class="Symbol">(</a><a id="1697" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="1702" href="Data.These.Base.html#1702" class="Bound">a</a><a id="1703" class="Symbol">)</a> <a id="1708" class="Symbol">(</a><a id="1709" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1715" href="Data.These.Base.html#1715" class="Bound">c</a> <a id="1717" href="Data.These.Base.html#1717" class="Bound">d</a><a id="1718" class="Symbol">)</a> <a id="1720" class="Symbol">=</a> <a id="1722" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1728" class="Symbol">(</a><a id="1729" href="Data.These.Base.html#1692" class="Bound">f</a> <a id="1731" class="Symbol">(</a><a id="1732" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1738" href="Data.These.Base.html#1702" class="Bound">a</a> <a id="1740" href="Data.These.Base.html#1715" class="Bound">c</a><a id="1741" class="Symbol">))</a> <a id="1744" class="Symbol">(</a><a id="1745" href="Data.These.Base.html#1694" class="Bound">g</a> <a id="1747" class="Symbol">(</a><a id="1748" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1753" href="Data.These.Base.html#1717" class="Bound">d</a><a id="1754" class="Symbol">))</a>
|
||
<a id="1757" href="Data.These.Base.html#1467" class="Function">alignWith</a> <a id="1767" href="Data.These.Base.html#1767" class="Bound">f</a> <a id="1769" href="Data.These.Base.html#1769" class="Bound">g</a> <a id="1771" class="Symbol">(</a><a id="1772" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1777" href="Data.These.Base.html#1777" class="Bound">b</a><a id="1778" class="Symbol">)</a> <a id="1783" class="Symbol">(</a><a id="1784" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="1789" href="Data.These.Base.html#1789" class="Bound">c</a><a id="1790" class="Symbol">)</a> <a id="1795" class="Symbol">=</a> <a id="1797" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1803" class="Symbol">(</a><a id="1804" href="Data.These.Base.html#1767" class="Bound">f</a> <a id="1806" class="Symbol">(</a><a id="1807" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1812" href="Data.These.Base.html#1789" class="Bound">c</a><a id="1813" class="Symbol">))</a> <a id="1816" class="Symbol">(</a><a id="1817" href="Data.These.Base.html#1769" class="Bound">g</a> <a id="1819" class="Symbol">(</a><a id="1820" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="1825" href="Data.These.Base.html#1777" class="Bound">b</a><a id="1826" class="Symbol">))</a>
|
||
<a id="1829" href="Data.These.Base.html#1467" class="Function">alignWith</a> <a id="1839" href="Data.These.Base.html#1839" class="Bound">f</a> <a id="1841" href="Data.These.Base.html#1841" class="Bound">g</a> <a id="1843" class="Symbol">(</a><a id="1844" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1849" href="Data.These.Base.html#1849" class="Bound">b</a><a id="1850" class="Symbol">)</a> <a id="1855" class="Symbol">(</a><a id="1856" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1861" href="Data.These.Base.html#1861" class="Bound">d</a><a id="1862" class="Symbol">)</a> <a id="1867" class="Symbol">=</a> <a id="1869" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1874" class="Symbol">(</a><a id="1875" href="Data.These.Base.html#1841" class="Bound">g</a> <a id="1877" class="Symbol">(</a><a id="1878" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1884" href="Data.These.Base.html#1849" class="Bound">b</a> <a id="1886" href="Data.These.Base.html#1861" class="Bound">d</a><a id="1887" class="Symbol">))</a>
|
||
<a id="1890" href="Data.These.Base.html#1467" class="Function">alignWith</a> <a id="1900" href="Data.These.Base.html#1900" class="Bound">f</a> <a id="1902" href="Data.These.Base.html#1902" class="Bound">g</a> <a id="1904" class="Symbol">(</a><a id="1905" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1910" href="Data.These.Base.html#1910" class="Bound">b</a><a id="1911" class="Symbol">)</a> <a id="1916" class="Symbol">(</a><a id="1917" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1923" href="Data.These.Base.html#1923" class="Bound">c</a> <a id="1925" href="Data.These.Base.html#1925" class="Bound">d</a><a id="1926" class="Symbol">)</a> <a id="1928" class="Symbol">=</a> <a id="1930" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1936" class="Symbol">(</a><a id="1937" href="Data.These.Base.html#1900" class="Bound">f</a> <a id="1939" class="Symbol">(</a><a id="1940" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="1945" href="Data.These.Base.html#1923" class="Bound">c</a><a id="1946" class="Symbol">))</a> <a id="1949" class="Symbol">(</a><a id="1950" href="Data.These.Base.html#1902" class="Bound">g</a> <a id="1952" class="Symbol">(</a><a id="1953" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1959" href="Data.These.Base.html#1910" class="Bound">b</a> <a id="1961" href="Data.These.Base.html#1925" class="Bound">d</a><a id="1962" class="Symbol">))</a>
|
||
<a id="1965" href="Data.These.Base.html#1467" class="Function">alignWith</a> <a id="1975" href="Data.These.Base.html#1975" class="Bound">f</a> <a id="1977" href="Data.These.Base.html#1977" class="Bound">g</a> <a id="1979" class="Symbol">(</a><a id="1980" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="1986" href="Data.These.Base.html#1986" class="Bound">a</a> <a id="1988" href="Data.These.Base.html#1988" class="Bound">b</a><a id="1989" class="Symbol">)</a> <a id="1991" class="Symbol">(</a><a id="1992" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="1997" href="Data.These.Base.html#1997" class="Bound">c</a><a id="1998" class="Symbol">)</a> <a id="2003" class="Symbol">=</a> <a id="2005" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="2011" class="Symbol">(</a><a id="2012" href="Data.These.Base.html#1975" class="Bound">f</a> <a id="2014" class="Symbol">(</a><a id="2015" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="2021" href="Data.These.Base.html#1986" class="Bound">a</a> <a id="2023" href="Data.These.Base.html#1997" class="Bound">c</a><a id="2024" class="Symbol">))</a> <a id="2027" class="Symbol">(</a><a id="2028" href="Data.These.Base.html#1977" class="Bound">g</a> <a id="2030" class="Symbol">(</a><a id="2031" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="2036" href="Data.These.Base.html#1988" class="Bound">b</a><a id="2037" class="Symbol">))</a>
|
||
<a id="2040" href="Data.These.Base.html#1467" class="Function">alignWith</a> <a id="2050" href="Data.These.Base.html#2050" class="Bound">f</a> <a id="2052" href="Data.These.Base.html#2052" class="Bound">g</a> <a id="2054" class="Symbol">(</a><a id="2055" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="2061" href="Data.These.Base.html#2061" class="Bound">a</a> <a id="2063" href="Data.These.Base.html#2063" class="Bound">b</a><a id="2064" class="Symbol">)</a> <a id="2066" class="Symbol">(</a><a id="2067" href="Data.These.Base.html#614" class="InductiveConstructor">that</a> <a id="2072" href="Data.These.Base.html#2072" class="Bound">d</a><a id="2073" class="Symbol">)</a> <a id="2078" class="Symbol">=</a> <a id="2080" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="2086" class="Symbol">(</a><a id="2087" href="Data.These.Base.html#2050" class="Bound">f</a> <a id="2089" class="Symbol">(</a><a id="2090" href="Data.These.Base.html#586" class="InductiveConstructor">this</a> <a id="2095" href="Data.These.Base.html#2061" class="Bound">a</a><a id="2096" class="Symbol">))</a> <a id="2099" class="Symbol">(</a><a id="2100" href="Data.These.Base.html#2052" class="Bound">g</a> <a id="2102" class="Symbol">(</a><a id="2103" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="2109" href="Data.These.Base.html#2063" class="Bound">b</a> <a id="2111" href="Data.These.Base.html#2072" class="Bound">d</a><a id="2112" class="Symbol">))</a>
|
||
<a id="2115" href="Data.These.Base.html#1467" class="Function">alignWith</a> <a id="2125" href="Data.These.Base.html#2125" class="Bound">f</a> <a id="2127" href="Data.These.Base.html#2127" class="Bound">g</a> <a id="2129" class="Symbol">(</a><a id="2130" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="2136" href="Data.These.Base.html#2136" class="Bound">a</a> <a id="2138" href="Data.These.Base.html#2138" class="Bound">b</a><a id="2139" class="Symbol">)</a> <a id="2141" class="Symbol">(</a><a id="2142" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="2148" href="Data.These.Base.html#2148" class="Bound">c</a> <a id="2150" href="Data.These.Base.html#2150" class="Bound">d</a><a id="2151" class="Symbol">)</a> <a id="2153" class="Symbol">=</a> <a id="2155" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="2161" class="Symbol">(</a><a id="2162" href="Data.These.Base.html#2125" class="Bound">f</a> <a id="2164" class="Symbol">(</a><a id="2165" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="2171" href="Data.These.Base.html#2136" class="Bound">a</a> <a id="2173" href="Data.These.Base.html#2148" class="Bound">c</a><a id="2174" class="Symbol">))</a> <a id="2177" class="Symbol">(</a><a id="2178" href="Data.These.Base.html#2127" class="Bound">g</a> <a id="2180" class="Symbol">(</a><a id="2181" href="Data.These.Base.html#642" class="InductiveConstructor">these</a> <a id="2187" href="Data.These.Base.html#2138" class="Bound">b</a> <a id="2189" href="Data.These.Base.html#2150" class="Bound">d</a><a id="2190" class="Symbol">))</a>
|
||
|
||
<a id="align"></a><a id="2194" href="Data.These.Base.html#2194" class="Function">align</a> <a id="2200" class="Symbol">:</a> <a id="2202" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="2208" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="2210" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="2212" class="Symbol">→</a> <a id="2214" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="2220" href="Data.These.Base.html#470" class="Generalizable">C</a> <a id="2222" href="Data.These.Base.html#484" class="Generalizable">D</a> <a id="2224" class="Symbol">→</a> <a id="2226" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="2232" class="Symbol">(</a><a id="2233" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="2239" href="Data.These.Base.html#442" class="Generalizable">A</a> <a id="2241" href="Data.These.Base.html#470" class="Generalizable">C</a><a id="2242" class="Symbol">)</a> <a id="2244" class="Symbol">(</a><a id="2245" href="Data.These.Base.html#528" class="Datatype">These</a> <a id="2251" href="Data.These.Base.html#456" class="Generalizable">B</a> <a id="2253" href="Data.These.Base.html#484" class="Generalizable">D</a><a id="2254" class="Symbol">)</a>
|
||
<a id="2256" href="Data.These.Base.html#2194" class="Function">align</a> <a id="2262" class="Symbol">=</a> <a id="2264" href="Data.These.Base.html#1467" class="Function">alignWith</a> <a id="2274" href="Function.Base.html#615" class="Function">id</a> <a id="2277" href="Function.Base.html#615" class="Function">id</a>
|
||
</pre></body></html> |