259 lines
77 KiB
HTML
259 lines
77 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Function.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">-- Simple combinators working solely on and with functions</a>
|
||
<a id="165" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="239" class="Comment">-- The contents of this file can be accessed from `Function`.</a>
|
||
|
||
<a id="302" class="Symbol">{-#</a> <a id="306" class="Keyword">OPTIONS</a> <a id="314" class="Pragma">--without-K</a> <a id="326" class="Pragma">--safe</a> <a id="333" class="Symbol">#-}</a>
|
||
|
||
<a id="338" class="Keyword">module</a> <a id="345" href="Function.Base.html" class="Module">Function.Base</a> <a id="359" class="Keyword">where</a>
|
||
|
||
<a id="366" class="Keyword">open</a> <a id="371" class="Keyword">import</a> <a id="378" href="Level.html" class="Module">Level</a>
|
||
<a id="384" class="Keyword">open</a> <a id="389" class="Keyword">import</a> <a id="396" href="Strict.html" class="Module">Strict</a>
|
||
|
||
<a id="404" class="Keyword">private</a>
|
||
<a id="414" class="Keyword">variable</a>
|
||
<a id="427" href="Function.Base.html#427" class="Generalizable">a</a> <a id="429" href="Function.Base.html#429" class="Generalizable">b</a> <a id="431" href="Function.Base.html#431" class="Generalizable">c</a> <a id="433" href="Function.Base.html#433" class="Generalizable">d</a> <a id="435" href="Function.Base.html#435" class="Generalizable">e</a> <a id="437" class="Symbol">:</a> <a id="439" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="449" href="Function.Base.html#449" class="Generalizable">A</a> <a id="451" class="Symbol">:</a> <a id="453" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="457" href="Function.Base.html#427" class="Generalizable">a</a>
|
||
<a id="463" href="Function.Base.html#463" class="Generalizable">B</a> <a id="465" class="Symbol">:</a> <a id="467" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="471" href="Function.Base.html#429" class="Generalizable">b</a>
|
||
<a id="477" href="Function.Base.html#477" class="Generalizable">C</a> <a id="479" class="Symbol">:</a> <a id="481" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="485" href="Function.Base.html#431" class="Generalizable">c</a>
|
||
<a id="491" href="Function.Base.html#491" class="Generalizable">D</a> <a id="493" class="Symbol">:</a> <a id="495" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="499" href="Function.Base.html#433" class="Generalizable">d</a>
|
||
<a id="505" href="Function.Base.html#505" class="Generalizable">E</a> <a id="507" class="Symbol">:</a> <a id="509" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="513" href="Function.Base.html#435" class="Generalizable">e</a>
|
||
|
||
<a id="516" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="589" class="Comment">-- Some simple functions</a>
|
||
|
||
<a id="id"></a><a id="615" href="Function.Base.html#615" class="Function">id</a> <a id="618" class="Symbol">:</a> <a id="620" href="Function.Base.html#449" class="Generalizable">A</a> <a id="622" class="Symbol">→</a> <a id="624" href="Function.Base.html#449" class="Generalizable">A</a>
|
||
<a id="626" href="Function.Base.html#615" class="Function">id</a> <a id="629" href="Function.Base.html#629" class="Bound">x</a> <a id="631" class="Symbol">=</a> <a id="633" href="Function.Base.html#629" class="Bound">x</a>
|
||
|
||
<a id="const"></a><a id="636" href="Function.Base.html#636" class="Function">const</a> <a id="642" class="Symbol">:</a> <a id="644" href="Function.Base.html#449" class="Generalizable">A</a> <a id="646" class="Symbol">→</a> <a id="648" href="Function.Base.html#463" class="Generalizable">B</a> <a id="650" class="Symbol">→</a> <a id="652" href="Function.Base.html#449" class="Generalizable">A</a>
|
||
<a id="654" href="Function.Base.html#636" class="Function">const</a> <a id="660" href="Function.Base.html#660" class="Bound">x</a> <a id="662" class="Symbol">=</a> <a id="664" class="Symbol">λ</a> <a id="666" href="Function.Base.html#666" class="Bound">_</a> <a id="668" class="Symbol">→</a> <a id="670" href="Function.Base.html#660" class="Bound">x</a>
|
||
|
||
<a id="constᵣ"></a><a id="673" href="Function.Base.html#673" class="Function">constᵣ</a> <a id="680" class="Symbol">:</a> <a id="682" href="Function.Base.html#449" class="Generalizable">A</a> <a id="684" class="Symbol">→</a> <a id="686" href="Function.Base.html#463" class="Generalizable">B</a> <a id="688" class="Symbol">→</a> <a id="690" href="Function.Base.html#463" class="Generalizable">B</a>
|
||
<a id="692" href="Function.Base.html#673" class="Function">constᵣ</a> <a id="699" class="Symbol">_</a> <a id="701" class="Symbol">=</a> <a id="703" href="Function.Base.html#615" class="Function">id</a>
|
||
|
||
<a id="707" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="780" class="Comment">-- Operations on dependent functions</a>
|
||
|
||
<a id="818" class="Comment">-- These are functions whose output has a type that depends on the</a>
|
||
<a id="885" class="Comment">-- value of the input to the function.</a>
|
||
|
||
<a id="925" class="Keyword">infixr</a> <a id="932" class="Number">9</a> <a id="934" href="Function.Base.html#1031" class="Function Operator">_∘_</a> <a id="938" href="Function.Base.html#1219" class="Function Operator">_∘₂_</a>
|
||
<a id="943" class="Keyword">infixl</a> <a id="950" class="Number">8</a> <a id="952" href="Function.Base.html#2477" class="Function Operator">_ˢ_</a>
|
||
<a id="956" class="Keyword">infixl</a> <a id="963" class="Number">0</a> <a id="965" href="Function.Base.html#2210" class="Function Operator">_|>_</a>
|
||
<a id="970" class="Keyword">infix</a> <a id="977" class="Number">0</a> <a id="979" href="Function.Base.html#3034" class="Function Operator">case_return_of_</a>
|
||
<a id="995" class="Keyword">infixr</a> <a id="1002" class="Number">-1</a> <a id="1005" href="Function.Base.html#1919" class="Function Operator">_$_</a> <a id="1009" href="Function.Base.html#2068" class="Function Operator">_$!_</a>
|
||
|
||
<a id="1015" class="Comment">-- Composition</a>
|
||
|
||
<a id="_∘_"></a><a id="1031" href="Function.Base.html#1031" class="Function Operator">_∘_</a> <a id="1035" class="Symbol">:</a> <a id="1037" class="Symbol">∀</a> <a id="1039" class="Symbol">{</a><a id="1040" href="Function.Base.html#1040" class="Bound">A</a> <a id="1042" class="Symbol">:</a> <a id="1044" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1048" href="Function.Base.html#427" class="Generalizable">a</a><a id="1049" class="Symbol">}</a> <a id="1051" class="Symbol">{</a><a id="1052" href="Function.Base.html#1052" class="Bound">B</a> <a id="1054" class="Symbol">:</a> <a id="1056" href="Function.Base.html#1040" class="Bound">A</a> <a id="1058" class="Symbol">→</a> <a id="1060" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1064" href="Function.Base.html#429" class="Generalizable">b</a><a id="1065" class="Symbol">}</a> <a id="1067" class="Symbol">{</a><a id="1068" href="Function.Base.html#1068" class="Bound">C</a> <a id="1070" class="Symbol">:</a> <a id="1072" class="Symbol">{</a><a id="1073" href="Function.Base.html#1073" class="Bound">x</a> <a id="1075" class="Symbol">:</a> <a id="1077" href="Function.Base.html#1040" class="Bound">A</a><a id="1078" class="Symbol">}</a> <a id="1080" class="Symbol">→</a> <a id="1082" href="Function.Base.html#1052" class="Bound">B</a> <a id="1084" href="Function.Base.html#1073" class="Bound">x</a> <a id="1086" class="Symbol">→</a> <a id="1088" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1092" href="Function.Base.html#431" class="Generalizable">c</a><a id="1093" class="Symbol">}</a> <a id="1095" class="Symbol">→</a>
|
||
<a id="1103" class="Symbol">(∀</a> <a id="1106" class="Symbol">{</a><a id="1107" href="Function.Base.html#1107" class="Bound">x</a><a id="1108" class="Symbol">}</a> <a id="1110" class="Symbol">(</a><a id="1111" href="Function.Base.html#1111" class="Bound">y</a> <a id="1113" class="Symbol">:</a> <a id="1115" href="Function.Base.html#1052" class="Bound">B</a> <a id="1117" href="Function.Base.html#1107" class="Bound">x</a><a id="1118" class="Symbol">)</a> <a id="1120" class="Symbol">→</a> <a id="1122" href="Function.Base.html#1068" class="Bound">C</a> <a id="1124" href="Function.Base.html#1111" class="Bound">y</a><a id="1125" class="Symbol">)</a> <a id="1127" class="Symbol">→</a> <a id="1129" class="Symbol">(</a><a id="1130" href="Function.Base.html#1130" class="Bound">g</a> <a id="1132" class="Symbol">:</a> <a id="1134" class="Symbol">(</a><a id="1135" href="Function.Base.html#1135" class="Bound">x</a> <a id="1137" class="Symbol">:</a> <a id="1139" href="Function.Base.html#1040" class="Bound">A</a><a id="1140" class="Symbol">)</a> <a id="1142" class="Symbol">→</a> <a id="1144" href="Function.Base.html#1052" class="Bound">B</a> <a id="1146" href="Function.Base.html#1135" class="Bound">x</a><a id="1147" class="Symbol">)</a> <a id="1149" class="Symbol">→</a>
|
||
<a id="1157" class="Symbol">((</a><a id="1159" href="Function.Base.html#1159" class="Bound">x</a> <a id="1161" class="Symbol">:</a> <a id="1163" href="Function.Base.html#1040" class="Bound">A</a><a id="1164" class="Symbol">)</a> <a id="1166" class="Symbol">→</a> <a id="1168" href="Function.Base.html#1068" class="Bound">C</a> <a id="1170" class="Symbol">(</a><a id="1171" href="Function.Base.html#1130" class="Bound">g</a> <a id="1173" href="Function.Base.html#1159" class="Bound">x</a><a id="1174" class="Symbol">))</a>
|
||
<a id="1177" href="Function.Base.html#1177" class="Bound">f</a> <a id="1179" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1181" href="Function.Base.html#1181" class="Bound">g</a> <a id="1183" class="Symbol">=</a> <a id="1185" class="Symbol">λ</a> <a id="1187" href="Function.Base.html#1187" class="Bound">x</a> <a id="1189" class="Symbol">→</a> <a id="1191" href="Function.Base.html#1177" class="Bound">f</a> <a id="1193" class="Symbol">(</a><a id="1194" href="Function.Base.html#1181" class="Bound">g</a> <a id="1196" href="Function.Base.html#1187" class="Bound">x</a><a id="1197" class="Symbol">)</a>
|
||
<a id="1199" class="Symbol">{-#</a> <a id="1203" class="Keyword">INLINE</a> <a id="1210" href="Function.Base.html#1031" class="Function Operator">_∘_</a> <a id="1214" class="Symbol">#-}</a>
|
||
|
||
<a id="_∘₂_"></a><a id="1219" href="Function.Base.html#1219" class="Function Operator">_∘₂_</a> <a id="1224" class="Symbol">:</a> <a id="1226" class="Symbol">∀</a> <a id="1228" class="Symbol">{</a><a id="1229" href="Function.Base.html#1229" class="Bound">A₁</a> <a id="1232" class="Symbol">:</a> <a id="1234" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1238" href="Function.Base.html#427" class="Generalizable">a</a><a id="1239" class="Symbol">}</a> <a id="1241" class="Symbol">{</a><a id="1242" href="Function.Base.html#1242" class="Bound">A₂</a> <a id="1245" class="Symbol">:</a> <a id="1247" href="Function.Base.html#1229" class="Bound">A₁</a> <a id="1250" class="Symbol">→</a> <a id="1252" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1256" href="Function.Base.html#433" class="Generalizable">d</a><a id="1257" class="Symbol">}</a>
|
||
<a id="1268" class="Symbol">{</a><a id="1269" href="Function.Base.html#1269" class="Bound">B</a> <a id="1271" class="Symbol">:</a> <a id="1273" class="Symbol">(</a><a id="1274" href="Function.Base.html#1274" class="Bound">x</a> <a id="1276" class="Symbol">:</a> <a id="1278" href="Function.Base.html#1229" class="Bound">A₁</a><a id="1280" class="Symbol">)</a> <a id="1282" class="Symbol">→</a> <a id="1284" href="Function.Base.html#1242" class="Bound">A₂</a> <a id="1287" href="Function.Base.html#1274" class="Bound">x</a> <a id="1289" class="Symbol">→</a> <a id="1291" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1295" href="Function.Base.html#429" class="Generalizable">b</a><a id="1296" class="Symbol">}</a>
|
||
<a id="1307" class="Symbol">{</a><a id="1308" href="Function.Base.html#1308" class="Bound">C</a> <a id="1310" class="Symbol">:</a> <a id="1312" class="Symbol">{</a><a id="1313" href="Function.Base.html#1313" class="Bound">x</a> <a id="1315" class="Symbol">:</a> <a id="1317" href="Function.Base.html#1229" class="Bound">A₁</a><a id="1319" class="Symbol">}</a> <a id="1321" class="Symbol">→</a> <a id="1323" class="Symbol">{</a><a id="1324" href="Function.Base.html#1324" class="Bound">y</a> <a id="1326" class="Symbol">:</a> <a id="1328" href="Function.Base.html#1242" class="Bound">A₂</a> <a id="1331" href="Function.Base.html#1313" class="Bound">x</a><a id="1332" class="Symbol">}</a> <a id="1334" class="Symbol">→</a> <a id="1336" href="Function.Base.html#1269" class="Bound">B</a> <a id="1338" href="Function.Base.html#1313" class="Bound">x</a> <a id="1340" href="Function.Base.html#1324" class="Bound">y</a> <a id="1342" class="Symbol">→</a> <a id="1344" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1348" href="Function.Base.html#431" class="Generalizable">c</a><a id="1349" class="Symbol">}</a> <a id="1351" class="Symbol">→</a>
|
||
<a id="1360" class="Symbol">({</a><a id="1362" href="Function.Base.html#1362" class="Bound">x</a> <a id="1364" class="Symbol">:</a> <a id="1366" href="Function.Base.html#1229" class="Bound">A₁</a><a id="1368" class="Symbol">}</a> <a id="1370" class="Symbol">→</a> <a id="1372" class="Symbol">{</a><a id="1373" href="Function.Base.html#1373" class="Bound">y</a> <a id="1375" class="Symbol">:</a> <a id="1377" href="Function.Base.html#1242" class="Bound">A₂</a> <a id="1380" href="Function.Base.html#1362" class="Bound">x</a><a id="1381" class="Symbol">}</a> <a id="1383" class="Symbol">→</a> <a id="1385" class="Symbol">(</a><a id="1386" href="Function.Base.html#1386" class="Bound">z</a> <a id="1388" class="Symbol">:</a> <a id="1390" href="Function.Base.html#1269" class="Bound">B</a> <a id="1392" href="Function.Base.html#1362" class="Bound">x</a> <a id="1394" href="Function.Base.html#1373" class="Bound">y</a><a id="1395" class="Symbol">)</a> <a id="1397" class="Symbol">→</a> <a id="1399" href="Function.Base.html#1308" class="Bound">C</a> <a id="1401" href="Function.Base.html#1386" class="Bound">z</a><a id="1402" class="Symbol">)</a> <a id="1404" class="Symbol">→</a>
|
||
<a id="1413" class="Symbol">(</a><a id="1414" href="Function.Base.html#1414" class="Bound">g</a> <a id="1416" class="Symbol">:</a> <a id="1418" class="Symbol">(</a><a id="1419" href="Function.Base.html#1419" class="Bound">x</a> <a id="1421" class="Symbol">:</a> <a id="1423" href="Function.Base.html#1229" class="Bound">A₁</a><a id="1425" class="Symbol">)</a> <a id="1427" class="Symbol">→</a> <a id="1429" class="Symbol">(</a><a id="1430" href="Function.Base.html#1430" class="Bound">y</a> <a id="1432" class="Symbol">:</a> <a id="1434" href="Function.Base.html#1242" class="Bound">A₂</a> <a id="1437" href="Function.Base.html#1419" class="Bound">x</a><a id="1438" class="Symbol">)</a> <a id="1440" class="Symbol">→</a> <a id="1442" href="Function.Base.html#1269" class="Bound">B</a> <a id="1444" href="Function.Base.html#1419" class="Bound">x</a> <a id="1446" href="Function.Base.html#1430" class="Bound">y</a><a id="1447" class="Symbol">)</a> <a id="1449" class="Symbol">→</a>
|
||
<a id="1458" class="Symbol">((</a><a id="1460" href="Function.Base.html#1460" class="Bound">x</a> <a id="1462" class="Symbol">:</a> <a id="1464" href="Function.Base.html#1229" class="Bound">A₁</a><a id="1466" class="Symbol">)</a> <a id="1468" class="Symbol">→</a> <a id="1470" class="Symbol">(</a><a id="1471" href="Function.Base.html#1471" class="Bound">y</a> <a id="1473" class="Symbol">:</a> <a id="1475" href="Function.Base.html#1242" class="Bound">A₂</a> <a id="1478" href="Function.Base.html#1460" class="Bound">x</a><a id="1479" class="Symbol">)</a> <a id="1481" class="Symbol">→</a> <a id="1483" href="Function.Base.html#1308" class="Bound">C</a> <a id="1485" class="Symbol">(</a><a id="1486" href="Function.Base.html#1414" class="Bound">g</a> <a id="1488" href="Function.Base.html#1460" class="Bound">x</a> <a id="1490" href="Function.Base.html#1471" class="Bound">y</a><a id="1491" class="Symbol">))</a>
|
||
<a id="1494" href="Function.Base.html#1494" class="Bound">f</a> <a id="1496" href="Function.Base.html#1219" class="Function Operator">∘₂</a> <a id="1499" href="Function.Base.html#1499" class="Bound">g</a> <a id="1501" class="Symbol">=</a> <a id="1503" class="Symbol">λ</a> <a id="1505" href="Function.Base.html#1505" class="Bound">x</a> <a id="1507" href="Function.Base.html#1507" class="Bound">y</a> <a id="1509" class="Symbol">→</a> <a id="1511" href="Function.Base.html#1494" class="Bound">f</a> <a id="1513" class="Symbol">(</a><a id="1514" href="Function.Base.html#1499" class="Bound">g</a> <a id="1516" href="Function.Base.html#1505" class="Bound">x</a> <a id="1518" href="Function.Base.html#1507" class="Bound">y</a><a id="1519" class="Symbol">)</a>
|
||
|
||
<a id="1522" class="Comment">-- Flipping order of arguments</a>
|
||
|
||
<a id="flip"></a><a id="1554" href="Function.Base.html#1554" class="Function">flip</a> <a id="1559" class="Symbol">:</a> <a id="1561" class="Symbol">∀</a> <a id="1563" class="Symbol">{</a><a id="1564" href="Function.Base.html#1564" class="Bound">A</a> <a id="1566" class="Symbol">:</a> <a id="1568" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1572" href="Function.Base.html#427" class="Generalizable">a</a><a id="1573" class="Symbol">}</a> <a id="1575" class="Symbol">{</a><a id="1576" href="Function.Base.html#1576" class="Bound">B</a> <a id="1578" class="Symbol">:</a> <a id="1580" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1584" href="Function.Base.html#429" class="Generalizable">b</a><a id="1585" class="Symbol">}</a> <a id="1587" class="Symbol">{</a><a id="1588" href="Function.Base.html#1588" class="Bound">C</a> <a id="1590" class="Symbol">:</a> <a id="1592" href="Function.Base.html#1564" class="Bound">A</a> <a id="1594" class="Symbol">→</a> <a id="1596" href="Function.Base.html#1576" class="Bound">B</a> <a id="1598" class="Symbol">→</a> <a id="1600" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1604" href="Function.Base.html#431" class="Generalizable">c</a><a id="1605" class="Symbol">}</a> <a id="1607" class="Symbol">→</a>
|
||
<a id="1616" class="Symbol">((</a><a id="1618" href="Function.Base.html#1618" class="Bound">x</a> <a id="1620" class="Symbol">:</a> <a id="1622" href="Function.Base.html#1564" class="Bound">A</a><a id="1623" class="Symbol">)</a> <a id="1625" class="Symbol">(</a><a id="1626" href="Function.Base.html#1626" class="Bound">y</a> <a id="1628" class="Symbol">:</a> <a id="1630" href="Function.Base.html#1576" class="Bound">B</a><a id="1631" class="Symbol">)</a> <a id="1633" class="Symbol">→</a> <a id="1635" href="Function.Base.html#1588" class="Bound">C</a> <a id="1637" href="Function.Base.html#1618" class="Bound">x</a> <a id="1639" href="Function.Base.html#1626" class="Bound">y</a><a id="1640" class="Symbol">)</a> <a id="1642" class="Symbol">→</a> <a id="1644" class="Symbol">((</a><a id="1646" href="Function.Base.html#1646" class="Bound">y</a> <a id="1648" class="Symbol">:</a> <a id="1650" href="Function.Base.html#1576" class="Bound">B</a><a id="1651" class="Symbol">)</a> <a id="1653" class="Symbol">(</a><a id="1654" href="Function.Base.html#1654" class="Bound">x</a> <a id="1656" class="Symbol">:</a> <a id="1658" href="Function.Base.html#1564" class="Bound">A</a><a id="1659" class="Symbol">)</a> <a id="1661" class="Symbol">→</a> <a id="1663" href="Function.Base.html#1588" class="Bound">C</a> <a id="1665" href="Function.Base.html#1654" class="Bound">x</a> <a id="1667" href="Function.Base.html#1646" class="Bound">y</a><a id="1668" class="Symbol">)</a>
|
||
<a id="1670" href="Function.Base.html#1554" class="Function">flip</a> <a id="1675" href="Function.Base.html#1675" class="Bound">f</a> <a id="1677" class="Symbol">=</a> <a id="1679" class="Symbol">λ</a> <a id="1681" href="Function.Base.html#1681" class="Bound">y</a> <a id="1683" href="Function.Base.html#1683" class="Bound">x</a> <a id="1685" class="Symbol">→</a> <a id="1687" href="Function.Base.html#1675" class="Bound">f</a> <a id="1689" href="Function.Base.html#1683" class="Bound">x</a> <a id="1691" href="Function.Base.html#1681" class="Bound">y</a>
|
||
<a id="1693" class="Symbol">{-#</a> <a id="1697" class="Keyword">INLINE</a> <a id="1704" href="Function.Base.html#1554" class="Function">flip</a> <a id="1709" class="Symbol">#-}</a>
|
||
|
||
<a id="1714" class="Comment">-- Application - note that _$_ is right associative, as in Haskell.</a>
|
||
<a id="1782" class="Comment">-- If you want a left associative infix application operator, use</a>
|
||
<a id="1848" class="Comment">-- Category.Functor._<$>_ from Category.Monad.Identity.IdentityMonad.</a>
|
||
|
||
<a id="_$_"></a><a id="1919" href="Function.Base.html#1919" class="Function Operator">_$_</a> <a id="1923" class="Symbol">:</a> <a id="1925" class="Symbol">∀</a> <a id="1927" class="Symbol">{</a><a id="1928" href="Function.Base.html#1928" class="Bound">A</a> <a id="1930" class="Symbol">:</a> <a id="1932" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1936" href="Function.Base.html#427" class="Generalizable">a</a><a id="1937" class="Symbol">}</a> <a id="1939" class="Symbol">{</a><a id="1940" href="Function.Base.html#1940" class="Bound">B</a> <a id="1942" class="Symbol">:</a> <a id="1944" href="Function.Base.html#1928" class="Bound">A</a> <a id="1946" class="Symbol">→</a> <a id="1948" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1952" href="Function.Base.html#429" class="Generalizable">b</a><a id="1953" class="Symbol">}</a> <a id="1955" class="Symbol">→</a>
|
||
<a id="1963" class="Symbol">((</a><a id="1965" href="Function.Base.html#1965" class="Bound">x</a> <a id="1967" class="Symbol">:</a> <a id="1969" href="Function.Base.html#1928" class="Bound">A</a><a id="1970" class="Symbol">)</a> <a id="1972" class="Symbol">→</a> <a id="1974" href="Function.Base.html#1940" class="Bound">B</a> <a id="1976" href="Function.Base.html#1965" class="Bound">x</a><a id="1977" class="Symbol">)</a> <a id="1979" class="Symbol">→</a> <a id="1981" class="Symbol">((</a><a id="1983" href="Function.Base.html#1983" class="Bound">x</a> <a id="1985" class="Symbol">:</a> <a id="1987" href="Function.Base.html#1928" class="Bound">A</a><a id="1988" class="Symbol">)</a> <a id="1990" class="Symbol">→</a> <a id="1992" href="Function.Base.html#1940" class="Bound">B</a> <a id="1994" href="Function.Base.html#1983" class="Bound">x</a><a id="1995" class="Symbol">)</a>
|
||
<a id="1997" href="Function.Base.html#1997" class="Bound">f</a> <a id="1999" href="Function.Base.html#1919" class="Function Operator">$</a> <a id="2001" href="Function.Base.html#2001" class="Bound">x</a> <a id="2003" class="Symbol">=</a> <a id="2005" href="Function.Base.html#1997" class="Bound">f</a> <a id="2007" href="Function.Base.html#2001" class="Bound">x</a>
|
||
<a id="2009" class="Symbol">{-#</a> <a id="2013" class="Keyword">INLINE</a> <a id="2020" href="Function.Base.html#1919" class="Function Operator">_$_</a> <a id="2024" class="Symbol">#-}</a>
|
||
|
||
<a id="2029" class="Comment">-- Strict (call-by-value) application</a>
|
||
|
||
<a id="_$!_"></a><a id="2068" href="Function.Base.html#2068" class="Function Operator">_$!_</a> <a id="2073" class="Symbol">:</a> <a id="2075" class="Symbol">∀</a> <a id="2077" class="Symbol">{</a><a id="2078" href="Function.Base.html#2078" class="Bound">A</a> <a id="2080" class="Symbol">:</a> <a id="2082" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2086" href="Function.Base.html#427" class="Generalizable">a</a><a id="2087" class="Symbol">}</a> <a id="2089" class="Symbol">{</a><a id="2090" href="Function.Base.html#2090" class="Bound">B</a> <a id="2092" class="Symbol">:</a> <a id="2094" href="Function.Base.html#2078" class="Bound">A</a> <a id="2096" class="Symbol">→</a> <a id="2098" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2102" href="Function.Base.html#429" class="Generalizable">b</a><a id="2103" class="Symbol">}</a> <a id="2105" class="Symbol">→</a>
|
||
<a id="2114" class="Symbol">((</a><a id="2116" href="Function.Base.html#2116" class="Bound">x</a> <a id="2118" class="Symbol">:</a> <a id="2120" href="Function.Base.html#2078" class="Bound">A</a><a id="2121" class="Symbol">)</a> <a id="2123" class="Symbol">→</a> <a id="2125" href="Function.Base.html#2090" class="Bound">B</a> <a id="2127" href="Function.Base.html#2116" class="Bound">x</a><a id="2128" class="Symbol">)</a> <a id="2130" class="Symbol">→</a> <a id="2132" class="Symbol">((</a><a id="2134" href="Function.Base.html#2134" class="Bound">x</a> <a id="2136" class="Symbol">:</a> <a id="2138" href="Function.Base.html#2078" class="Bound">A</a><a id="2139" class="Symbol">)</a> <a id="2141" class="Symbol">→</a> <a id="2143" href="Function.Base.html#2090" class="Bound">B</a> <a id="2145" href="Function.Base.html#2134" class="Bound">x</a><a id="2146" class="Symbol">)</a>
|
||
<a id="2148" href="Function.Base.html#2068" class="Function Operator">_$!_</a> <a id="2153" class="Symbol">=</a> <a id="2155" href="Function.Base.html#1554" class="Function">flip</a> <a id="2160" href="Agda.Builtin.Strict.html#179" class="Primitive">force</a>
|
||
|
||
<a id="2167" class="Comment">-- Flipped application (aka pipe-forward)</a>
|
||
|
||
<a id="_|>_"></a><a id="2210" href="Function.Base.html#2210" class="Function Operator">_|>_</a> <a id="2215" class="Symbol">:</a> <a id="2217" class="Symbol">∀</a> <a id="2219" class="Symbol">{</a><a id="2220" href="Function.Base.html#2220" class="Bound">A</a> <a id="2222" class="Symbol">:</a> <a id="2224" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2228" href="Function.Base.html#427" class="Generalizable">a</a><a id="2229" class="Symbol">}</a> <a id="2231" class="Symbol">{</a><a id="2232" href="Function.Base.html#2232" class="Bound">B</a> <a id="2234" class="Symbol">:</a> <a id="2236" href="Function.Base.html#2220" class="Bound">A</a> <a id="2238" class="Symbol">→</a> <a id="2240" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2244" href="Function.Base.html#429" class="Generalizable">b</a><a id="2245" class="Symbol">}</a> <a id="2247" class="Symbol">→</a>
|
||
<a id="2256" class="Symbol">(</a><a id="2257" href="Function.Base.html#2257" class="Bound">a</a> <a id="2259" class="Symbol">:</a> <a id="2261" href="Function.Base.html#2220" class="Bound">A</a><a id="2262" class="Symbol">)</a> <a id="2264" class="Symbol">→</a> <a id="2266" class="Symbol">(∀</a> <a id="2269" href="Function.Base.html#2269" class="Bound">a</a> <a id="2271" class="Symbol">→</a> <a id="2273" href="Function.Base.html#2232" class="Bound">B</a> <a id="2275" href="Function.Base.html#2269" class="Bound">a</a><a id="2276" class="Symbol">)</a> <a id="2278" class="Symbol">→</a> <a id="2280" href="Function.Base.html#2232" class="Bound">B</a> <a id="2282" href="Function.Base.html#2257" class="Bound">a</a>
|
||
<a id="2284" href="Function.Base.html#2210" class="Function Operator">_|>_</a> <a id="2289" class="Symbol">=</a> <a id="2291" href="Function.Base.html#1554" class="Function">flip</a> <a id="2296" href="Function.Base.html#1919" class="Function Operator">_$_</a>
|
||
<a id="2300" class="Symbol">{-#</a> <a id="2304" class="Keyword">INLINE</a> <a id="2311" href="Function.Base.html#2210" class="Function Operator">_|>_</a> <a id="2316" class="Symbol">#-}</a>
|
||
|
||
<a id="2321" class="Comment">-- The S combinator - written infix as in Conor McBride's paper</a>
|
||
<a id="2385" class="Comment">-- "Outrageous but Meaningful Coincidences: Dependent type-safe syntax</a>
|
||
<a id="2456" class="Comment">-- and evaluation".</a>
|
||
|
||
<a id="_ˢ_"></a><a id="2477" href="Function.Base.html#2477" class="Function Operator">_ˢ_</a> <a id="2481" class="Symbol">:</a> <a id="2483" class="Symbol">∀</a> <a id="2485" class="Symbol">{</a><a id="2486" href="Function.Base.html#2486" class="Bound">A</a> <a id="2488" class="Symbol">:</a> <a id="2490" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2494" href="Function.Base.html#427" class="Generalizable">a</a><a id="2495" class="Symbol">}</a> <a id="2497" class="Symbol">{</a><a id="2498" href="Function.Base.html#2498" class="Bound">B</a> <a id="2500" class="Symbol">:</a> <a id="2502" href="Function.Base.html#2486" class="Bound">A</a> <a id="2504" class="Symbol">→</a> <a id="2506" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2510" href="Function.Base.html#429" class="Generalizable">b</a><a id="2511" class="Symbol">}</a> <a id="2513" class="Symbol">{</a><a id="2514" href="Function.Base.html#2514" class="Bound">C</a> <a id="2516" class="Symbol">:</a> <a id="2518" class="Symbol">(</a><a id="2519" href="Function.Base.html#2519" class="Bound">x</a> <a id="2521" class="Symbol">:</a> <a id="2523" href="Function.Base.html#2486" class="Bound">A</a><a id="2524" class="Symbol">)</a> <a id="2526" class="Symbol">→</a> <a id="2528" href="Function.Base.html#2498" class="Bound">B</a> <a id="2530" href="Function.Base.html#2519" class="Bound">x</a> <a id="2532" class="Symbol">→</a> <a id="2534" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2538" href="Function.Base.html#431" class="Generalizable">c</a><a id="2539" class="Symbol">}</a> <a id="2541" class="Symbol">→</a>
|
||
<a id="2549" class="Symbol">((</a><a id="2551" href="Function.Base.html#2551" class="Bound">x</a> <a id="2553" class="Symbol">:</a> <a id="2555" href="Function.Base.html#2486" class="Bound">A</a><a id="2556" class="Symbol">)</a> <a id="2558" class="Symbol">(</a><a id="2559" href="Function.Base.html#2559" class="Bound">y</a> <a id="2561" class="Symbol">:</a> <a id="2563" href="Function.Base.html#2498" class="Bound">B</a> <a id="2565" href="Function.Base.html#2551" class="Bound">x</a><a id="2566" class="Symbol">)</a> <a id="2568" class="Symbol">→</a> <a id="2570" href="Function.Base.html#2514" class="Bound">C</a> <a id="2572" href="Function.Base.html#2551" class="Bound">x</a> <a id="2574" href="Function.Base.html#2559" class="Bound">y</a><a id="2575" class="Symbol">)</a> <a id="2577" class="Symbol">→</a>
|
||
<a id="2585" class="Symbol">(</a><a id="2586" href="Function.Base.html#2586" class="Bound">g</a> <a id="2588" class="Symbol">:</a> <a id="2590" class="Symbol">(</a><a id="2591" href="Function.Base.html#2591" class="Bound">x</a> <a id="2593" class="Symbol">:</a> <a id="2595" href="Function.Base.html#2486" class="Bound">A</a><a id="2596" class="Symbol">)</a> <a id="2598" class="Symbol">→</a> <a id="2600" href="Function.Base.html#2498" class="Bound">B</a> <a id="2602" href="Function.Base.html#2591" class="Bound">x</a><a id="2603" class="Symbol">)</a> <a id="2605" class="Symbol">→</a>
|
||
<a id="2613" class="Symbol">((</a><a id="2615" href="Function.Base.html#2615" class="Bound">x</a> <a id="2617" class="Symbol">:</a> <a id="2619" href="Function.Base.html#2486" class="Bound">A</a><a id="2620" class="Symbol">)</a> <a id="2622" class="Symbol">→</a> <a id="2624" href="Function.Base.html#2514" class="Bound">C</a> <a id="2626" href="Function.Base.html#2615" class="Bound">x</a> <a id="2628" class="Symbol">(</a><a id="2629" href="Function.Base.html#2586" class="Bound">g</a> <a id="2631" href="Function.Base.html#2615" class="Bound">x</a><a id="2632" class="Symbol">))</a>
|
||
<a id="2635" href="Function.Base.html#2635" class="Bound">f</a> <a id="2637" href="Function.Base.html#2477" class="Function Operator">ˢ</a> <a id="2639" href="Function.Base.html#2639" class="Bound">g</a> <a id="2641" class="Symbol">=</a> <a id="2643" class="Symbol">λ</a> <a id="2645" href="Function.Base.html#2645" class="Bound">x</a> <a id="2647" class="Symbol">→</a> <a id="2649" href="Function.Base.html#2635" class="Bound">f</a> <a id="2651" href="Function.Base.html#2645" class="Bound">x</a> <a id="2653" class="Symbol">(</a><a id="2654" href="Function.Base.html#2639" class="Bound">g</a> <a id="2656" href="Function.Base.html#2645" class="Bound">x</a><a id="2657" class="Symbol">)</a>
|
||
<a id="2659" class="Symbol">{-#</a> <a id="2663" class="Keyword">INLINE</a> <a id="2670" href="Function.Base.html#2477" class="Function Operator">_ˢ_</a> <a id="2674" class="Symbol">#-}</a>
|
||
|
||
<a id="2679" class="Comment">-- Converting between implicit and explicit function spaces.</a>
|
||
|
||
<a id="_$-"></a><a id="2741" href="Function.Base.html#2741" class="Function Operator">_$-</a> <a id="2745" class="Symbol">:</a> <a id="2747" class="Symbol">∀</a> <a id="2749" class="Symbol">{</a><a id="2750" href="Function.Base.html#2750" class="Bound">A</a> <a id="2752" class="Symbol">:</a> <a id="2754" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2758" href="Function.Base.html#427" class="Generalizable">a</a><a id="2759" class="Symbol">}</a> <a id="2761" class="Symbol">{</a><a id="2762" href="Function.Base.html#2762" class="Bound">B</a> <a id="2764" class="Symbol">:</a> <a id="2766" href="Function.Base.html#2750" class="Bound">A</a> <a id="2768" class="Symbol">→</a> <a id="2770" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2774" href="Function.Base.html#429" class="Generalizable">b</a><a id="2775" class="Symbol">}</a> <a id="2777" class="Symbol">→</a> <a id="2779" class="Symbol">((</a><a id="2781" href="Function.Base.html#2781" class="Bound">x</a> <a id="2783" class="Symbol">:</a> <a id="2785" href="Function.Base.html#2750" class="Bound">A</a><a id="2786" class="Symbol">)</a> <a id="2788" class="Symbol">→</a> <a id="2790" href="Function.Base.html#2762" class="Bound">B</a> <a id="2792" href="Function.Base.html#2781" class="Bound">x</a><a id="2793" class="Symbol">)</a> <a id="2795" class="Symbol">→</a> <a id="2797" class="Symbol">({</a><a id="2799" href="Function.Base.html#2799" class="Bound">x</a> <a id="2801" class="Symbol">:</a> <a id="2803" href="Function.Base.html#2750" class="Bound">A</a><a id="2804" class="Symbol">}</a> <a id="2806" class="Symbol">→</a> <a id="2808" href="Function.Base.html#2762" class="Bound">B</a> <a id="2810" href="Function.Base.html#2799" class="Bound">x</a><a id="2811" class="Symbol">)</a>
|
||
<a id="2813" href="Function.Base.html#2813" class="Bound">f</a> <a id="2815" href="Function.Base.html#2741" class="Function Operator">$-</a> <a id="2818" class="Symbol">=</a> <a id="2820" href="Function.Base.html#2813" class="Bound">f</a> <a id="2822" class="Symbol">_</a>
|
||
<a id="2824" class="Symbol">{-#</a> <a id="2828" class="Keyword">INLINE</a> <a id="2835" href="Function.Base.html#2741" class="Function Operator">_$-</a> <a id="2839" class="Symbol">#-}</a>
|
||
|
||
<a id="λ-"></a><a id="2844" href="Function.Base.html#2844" class="Function">λ-</a> <a id="2847" class="Symbol">:</a> <a id="2849" class="Symbol">∀</a> <a id="2851" class="Symbol">{</a><a id="2852" href="Function.Base.html#2852" class="Bound">A</a> <a id="2854" class="Symbol">:</a> <a id="2856" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2860" href="Function.Base.html#427" class="Generalizable">a</a><a id="2861" class="Symbol">}</a> <a id="2863" class="Symbol">{</a><a id="2864" href="Function.Base.html#2864" class="Bound">B</a> <a id="2866" class="Symbol">:</a> <a id="2868" href="Function.Base.html#2852" class="Bound">A</a> <a id="2870" class="Symbol">→</a> <a id="2872" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2876" href="Function.Base.html#429" class="Generalizable">b</a><a id="2877" class="Symbol">}</a> <a id="2879" class="Symbol">→</a> <a id="2881" class="Symbol">({</a><a id="2883" href="Function.Base.html#2883" class="Bound">x</a> <a id="2885" class="Symbol">:</a> <a id="2887" href="Function.Base.html#2852" class="Bound">A</a><a id="2888" class="Symbol">}</a> <a id="2890" class="Symbol">→</a> <a id="2892" href="Function.Base.html#2864" class="Bound">B</a> <a id="2894" href="Function.Base.html#2883" class="Bound">x</a><a id="2895" class="Symbol">)</a> <a id="2897" class="Symbol">→</a> <a id="2899" class="Symbol">((</a><a id="2901" href="Function.Base.html#2901" class="Bound">x</a> <a id="2903" class="Symbol">:</a> <a id="2905" href="Function.Base.html#2852" class="Bound">A</a><a id="2906" class="Symbol">)</a> <a id="2908" class="Symbol">→</a> <a id="2910" href="Function.Base.html#2864" class="Bound">B</a> <a id="2912" href="Function.Base.html#2901" class="Bound">x</a><a id="2913" class="Symbol">)</a>
|
||
<a id="2915" href="Function.Base.html#2844" class="Function">λ-</a> <a id="2918" href="Function.Base.html#2918" class="Bound">f</a> <a id="2920" class="Symbol">=</a> <a id="2922" class="Symbol">λ</a> <a id="2924" href="Function.Base.html#2924" class="Bound">x</a> <a id="2926" class="Symbol">→</a> <a id="2928" href="Function.Base.html#2918" class="Bound">f</a>
|
||
<a id="2930" class="Symbol">{-#</a> <a id="2934" class="Keyword">INLINE</a> <a id="2941" href="Function.Base.html#2844" class="Function">λ-</a> <a id="2944" class="Symbol">#-}</a>
|
||
|
||
<a id="2949" class="Comment">-- Case expressions (to be used with pattern-matching lambdas, see</a>
|
||
<a id="3016" class="Comment">-- README.Case).</a>
|
||
|
||
<a id="case_return_of_"></a><a id="3034" href="Function.Base.html#3034" class="Function Operator">case_return_of_</a> <a id="3050" class="Symbol">:</a> <a id="3052" class="Symbol">∀</a> <a id="3054" class="Symbol">{</a><a id="3055" href="Function.Base.html#3055" class="Bound">A</a> <a id="3057" class="Symbol">:</a> <a id="3059" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3063" href="Function.Base.html#427" class="Generalizable">a</a><a id="3064" class="Symbol">}</a> <a id="3066" class="Symbol">(</a><a id="3067" href="Function.Base.html#3067" class="Bound">x</a> <a id="3069" class="Symbol">:</a> <a id="3071" href="Function.Base.html#3055" class="Bound">A</a><a id="3072" class="Symbol">)</a> <a id="3074" class="Symbol">(</a><a id="3075" href="Function.Base.html#3075" class="Bound">B</a> <a id="3077" class="Symbol">:</a> <a id="3079" href="Function.Base.html#3055" class="Bound">A</a> <a id="3081" class="Symbol">→</a> <a id="3083" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3087" href="Function.Base.html#429" class="Generalizable">b</a><a id="3088" class="Symbol">)</a> <a id="3090" class="Symbol">→</a>
|
||
<a id="3110" class="Symbol">((</a><a id="3112" href="Function.Base.html#3112" class="Bound">x</a> <a id="3114" class="Symbol">:</a> <a id="3116" href="Function.Base.html#3055" class="Bound">A</a><a id="3117" class="Symbol">)</a> <a id="3119" class="Symbol">→</a> <a id="3121" href="Function.Base.html#3075" class="Bound">B</a> <a id="3123" href="Function.Base.html#3112" class="Bound">x</a><a id="3124" class="Symbol">)</a> <a id="3126" class="Symbol">→</a> <a id="3128" href="Function.Base.html#3075" class="Bound">B</a> <a id="3130" href="Function.Base.html#3067" class="Bound">x</a>
|
||
<a id="3132" href="Function.Base.html#3034" class="Function Operator">case</a> <a id="3137" href="Function.Base.html#3137" class="Bound">x</a> <a id="3139" href="Function.Base.html#3034" class="Function Operator">return</a> <a id="3146" href="Function.Base.html#3146" class="Bound">B</a> <a id="3148" href="Function.Base.html#3034" class="Function Operator">of</a> <a id="3151" href="Function.Base.html#3151" class="Bound">f</a> <a id="3153" class="Symbol">=</a> <a id="3155" href="Function.Base.html#3151" class="Bound">f</a> <a id="3157" href="Function.Base.html#3137" class="Bound">x</a>
|
||
<a id="3159" class="Symbol">{-#</a> <a id="3163" class="Keyword">INLINE</a> <a id="3170" href="Function.Base.html#3034" class="Function Operator">case_return_of_</a> <a id="3186" class="Symbol">#-}</a>
|
||
|
||
<a id="3191" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="3264" class="Comment">-- Non-dependent versions of dependent operations</a>
|
||
|
||
<a id="3315" class="Comment">-- Any of the above operations for dependent functions will also work</a>
|
||
<a id="3385" class="Comment">-- for non-dependent functions but sometimes Agda has difficulty</a>
|
||
<a id="3450" class="Comment">-- inferring the non-dependency. Primed (′ = \prime) versions of the</a>
|
||
<a id="3519" class="Comment">-- operations are therefore provided below that sometimes have better</a>
|
||
<a id="3589" class="Comment">-- inference properties.</a>
|
||
|
||
<a id="3615" class="Keyword">infixr</a> <a id="3622" class="Number">9</a> <a id="3624" href="Function.Base.html#3706" class="Function Operator">_∘′_</a> <a id="3629" href="Function.Base.html#3759" class="Function Operator">_∘₂′_</a>
|
||
<a id="3635" class="Keyword">infixl</a> <a id="3642" class="Number">0</a> <a id="3644" href="Function.Base.html#3998" class="Function Operator">_|>′_</a>
|
||
<a id="3650" class="Keyword">infix</a> <a id="3657" class="Number">0</a> <a id="3659" href="Function.Base.html#4121" class="Function Operator">case_of_</a>
|
||
<a id="3668" class="Keyword">infixr</a> <a id="3675" class="Number">-1</a> <a id="3678" href="Function.Base.html#3839" class="Function Operator">_$′_</a> <a id="3683" href="Function.Base.html#3915" class="Function Operator">_$!′_</a>
|
||
|
||
<a id="3690" class="Comment">-- Composition</a>
|
||
|
||
<a id="_∘′_"></a><a id="3706" href="Function.Base.html#3706" class="Function Operator">_∘′_</a> <a id="3711" class="Symbol">:</a> <a id="3713" class="Symbol">(</a><a id="3714" href="Function.Base.html#463" class="Generalizable">B</a> <a id="3716" class="Symbol">→</a> <a id="3718" href="Function.Base.html#477" class="Generalizable">C</a><a id="3719" class="Symbol">)</a> <a id="3721" class="Symbol">→</a> <a id="3723" class="Symbol">(</a><a id="3724" href="Function.Base.html#449" class="Generalizable">A</a> <a id="3726" class="Symbol">→</a> <a id="3728" href="Function.Base.html#463" class="Generalizable">B</a><a id="3729" class="Symbol">)</a> <a id="3731" class="Symbol">→</a> <a id="3733" class="Symbol">(</a><a id="3734" href="Function.Base.html#449" class="Generalizable">A</a> <a id="3736" class="Symbol">→</a> <a id="3738" href="Function.Base.html#477" class="Generalizable">C</a><a id="3739" class="Symbol">)</a>
|
||
<a id="3741" href="Function.Base.html#3741" class="Bound">f</a> <a id="3743" href="Function.Base.html#3706" class="Function Operator">∘′</a> <a id="3746" href="Function.Base.html#3746" class="Bound">g</a> <a id="3748" class="Symbol">=</a> <a id="3750" href="Function.Base.html#1031" class="Function Operator">_∘_</a> <a id="3754" href="Function.Base.html#3741" class="Bound">f</a> <a id="3756" href="Function.Base.html#3746" class="Bound">g</a>
|
||
|
||
<a id="_∘₂′_"></a><a id="3759" href="Function.Base.html#3759" class="Function Operator">_∘₂′_</a> <a id="3765" class="Symbol">:</a> <a id="3767" class="Symbol">(</a><a id="3768" href="Function.Base.html#477" class="Generalizable">C</a> <a id="3770" class="Symbol">→</a> <a id="3772" href="Function.Base.html#491" class="Generalizable">D</a><a id="3773" class="Symbol">)</a> <a id="3775" class="Symbol">→</a> <a id="3777" class="Symbol">(</a><a id="3778" href="Function.Base.html#449" class="Generalizable">A</a> <a id="3780" class="Symbol">→</a> <a id="3782" href="Function.Base.html#463" class="Generalizable">B</a> <a id="3784" class="Symbol">→</a> <a id="3786" href="Function.Base.html#477" class="Generalizable">C</a><a id="3787" class="Symbol">)</a> <a id="3789" class="Symbol">→</a> <a id="3791" class="Symbol">(</a><a id="3792" href="Function.Base.html#449" class="Generalizable">A</a> <a id="3794" class="Symbol">→</a> <a id="3796" href="Function.Base.html#463" class="Generalizable">B</a> <a id="3798" class="Symbol">→</a> <a id="3800" href="Function.Base.html#491" class="Generalizable">D</a><a id="3801" class="Symbol">)</a>
|
||
<a id="3803" href="Function.Base.html#3803" class="Bound">f</a> <a id="3805" href="Function.Base.html#3759" class="Function Operator">∘₂′</a> <a id="3809" href="Function.Base.html#3809" class="Bound">g</a> <a id="3811" class="Symbol">=</a> <a id="3813" href="Function.Base.html#1219" class="Function Operator">_∘₂_</a> <a id="3818" href="Function.Base.html#3803" class="Bound">f</a> <a id="3820" href="Function.Base.html#3809" class="Bound">g</a>
|
||
|
||
<a id="3823" class="Comment">-- Application</a>
|
||
|
||
<a id="_$′_"></a><a id="3839" href="Function.Base.html#3839" class="Function Operator">_$′_</a> <a id="3844" class="Symbol">:</a> <a id="3846" class="Symbol">(</a><a id="3847" href="Function.Base.html#449" class="Generalizable">A</a> <a id="3849" class="Symbol">→</a> <a id="3851" href="Function.Base.html#463" class="Generalizable">B</a><a id="3852" class="Symbol">)</a> <a id="3854" class="Symbol">→</a> <a id="3856" class="Symbol">(</a><a id="3857" href="Function.Base.html#449" class="Generalizable">A</a> <a id="3859" class="Symbol">→</a> <a id="3861" href="Function.Base.html#463" class="Generalizable">B</a><a id="3862" class="Symbol">)</a>
|
||
<a id="3864" href="Function.Base.html#3839" class="Function Operator">_$′_</a> <a id="3869" class="Symbol">=</a> <a id="3871" href="Function.Base.html#1919" class="Function Operator">_$_</a>
|
||
|
||
<a id="3876" class="Comment">-- Strict (call-by-value) application</a>
|
||
|
||
<a id="_$!′_"></a><a id="3915" href="Function.Base.html#3915" class="Function Operator">_$!′_</a> <a id="3921" class="Symbol">:</a> <a id="3923" class="Symbol">(</a><a id="3924" href="Function.Base.html#449" class="Generalizable">A</a> <a id="3926" class="Symbol">→</a> <a id="3928" href="Function.Base.html#463" class="Generalizable">B</a><a id="3929" class="Symbol">)</a> <a id="3931" class="Symbol">→</a> <a id="3933" class="Symbol">(</a><a id="3934" href="Function.Base.html#449" class="Generalizable">A</a> <a id="3936" class="Symbol">→</a> <a id="3938" href="Function.Base.html#463" class="Generalizable">B</a><a id="3939" class="Symbol">)</a>
|
||
<a id="3941" href="Function.Base.html#3915" class="Function Operator">_$!′_</a> <a id="3947" class="Symbol">=</a> <a id="3949" href="Function.Base.html#2068" class="Function Operator">_$!_</a>
|
||
|
||
<a id="3955" class="Comment">-- Flipped application (aka pipe-forward)</a>
|
||
|
||
<a id="_|>′_"></a><a id="3998" href="Function.Base.html#3998" class="Function Operator">_|>′_</a> <a id="4004" class="Symbol">:</a> <a id="4006" href="Function.Base.html#449" class="Generalizable">A</a> <a id="4008" class="Symbol">→</a> <a id="4010" class="Symbol">(</a><a id="4011" href="Function.Base.html#449" class="Generalizable">A</a> <a id="4013" class="Symbol">→</a> <a id="4015" href="Function.Base.html#463" class="Generalizable">B</a><a id="4016" class="Symbol">)</a> <a id="4018" class="Symbol">→</a> <a id="4020" href="Function.Base.html#463" class="Generalizable">B</a>
|
||
<a id="4022" href="Function.Base.html#3998" class="Function Operator">_|>′_</a> <a id="4028" class="Symbol">=</a> <a id="4030" href="Function.Base.html#2210" class="Function Operator">_|>_</a>
|
||
|
||
<a id="4036" class="Comment">-- Case expressions (to be used with pattern-matching lambdas, see</a>
|
||
<a id="4103" class="Comment">-- README.Case).</a>
|
||
|
||
<a id="case_of_"></a><a id="4121" href="Function.Base.html#4121" class="Function Operator">case_of_</a> <a id="4130" class="Symbol">:</a> <a id="4132" href="Function.Base.html#449" class="Generalizable">A</a> <a id="4134" class="Symbol">→</a> <a id="4136" class="Symbol">(</a><a id="4137" href="Function.Base.html#449" class="Generalizable">A</a> <a id="4139" class="Symbol">→</a> <a id="4141" href="Function.Base.html#463" class="Generalizable">B</a><a id="4142" class="Symbol">)</a> <a id="4144" class="Symbol">→</a> <a id="4146" href="Function.Base.html#463" class="Generalizable">B</a>
|
||
<a id="4148" href="Function.Base.html#4121" class="Function Operator">case</a> <a id="4153" href="Function.Base.html#4153" class="Bound">x</a> <a id="4155" href="Function.Base.html#4121" class="Function Operator">of</a> <a id="4158" href="Function.Base.html#4158" class="Bound">f</a> <a id="4160" class="Symbol">=</a> <a id="4162" href="Function.Base.html#3034" class="Function Operator">case</a> <a id="4167" href="Function.Base.html#4153" class="Bound">x</a> <a id="4169" href="Function.Base.html#3034" class="Function Operator">return</a> <a id="4176" class="Symbol">_</a> <a id="4178" href="Function.Base.html#3034" class="Function Operator">of</a> <a id="4181" href="Function.Base.html#4158" class="Bound">f</a>
|
||
<a id="4183" class="Symbol">{-#</a> <a id="4187" class="Keyword">INLINE</a> <a id="4194" href="Function.Base.html#4121" class="Function Operator">case_of_</a> <a id="4203" class="Symbol">#-}</a>
|
||
|
||
<a id="4208" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="4281" class="Comment">-- Operations that are only defined for non-dependent functions</a>
|
||
|
||
<a id="4346" class="Keyword">infixl</a> <a id="4353" class="Number">1</a> <a id="4355" href="Function.Base.html#4398" class="Function Operator">_⟨_⟩_</a>
|
||
<a id="4361" class="Keyword">infixl</a> <a id="4368" class="Number">0</a> <a id="4370" href="Function.Base.html#4562" class="Function Operator">_∋_</a>
|
||
|
||
<a id="4375" class="Comment">-- Binary application</a>
|
||
|
||
<a id="_⟨_⟩_"></a><a id="4398" href="Function.Base.html#4398" class="Function Operator">_⟨_⟩_</a> <a id="4404" class="Symbol">:</a> <a id="4406" href="Function.Base.html#449" class="Generalizable">A</a> <a id="4408" class="Symbol">→</a> <a id="4410" class="Symbol">(</a><a id="4411" href="Function.Base.html#449" class="Generalizable">A</a> <a id="4413" class="Symbol">→</a> <a id="4415" href="Function.Base.html#463" class="Generalizable">B</a> <a id="4417" class="Symbol">→</a> <a id="4419" href="Function.Base.html#477" class="Generalizable">C</a><a id="4420" class="Symbol">)</a> <a id="4422" class="Symbol">→</a> <a id="4424" href="Function.Base.html#463" class="Generalizable">B</a> <a id="4426" class="Symbol">→</a> <a id="4428" href="Function.Base.html#477" class="Generalizable">C</a>
|
||
<a id="4430" href="Function.Base.html#4430" class="Bound">x</a> <a id="4432" href="Function.Base.html#4398" class="Function Operator">⟨</a> <a id="4434" href="Function.Base.html#4434" class="Bound">f</a> <a id="4436" href="Function.Base.html#4398" class="Function Operator">⟩</a> <a id="4438" href="Function.Base.html#4438" class="Bound">y</a> <a id="4440" class="Symbol">=</a> <a id="4442" href="Function.Base.html#4434" class="Bound">f</a> <a id="4444" href="Function.Base.html#4430" class="Bound">x</a> <a id="4446" href="Function.Base.html#4438" class="Bound">y</a>
|
||
|
||
<a id="4449" class="Comment">-- In Agda you cannot annotate every subexpression with a type</a>
|
||
<a id="4512" class="Comment">-- signature. This function can be used instead.</a>
|
||
|
||
<a id="_∋_"></a><a id="4562" href="Function.Base.html#4562" class="Function Operator">_∋_</a> <a id="4566" class="Symbol">:</a> <a id="4568" class="Symbol">(</a><a id="4569" href="Function.Base.html#4569" class="Bound">A</a> <a id="4571" class="Symbol">:</a> <a id="4573" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4577" href="Function.Base.html#427" class="Generalizable">a</a><a id="4578" class="Symbol">)</a> <a id="4580" class="Symbol">→</a> <a id="4582" href="Function.Base.html#4569" class="Bound">A</a> <a id="4584" class="Symbol">→</a> <a id="4586" href="Function.Base.html#4569" class="Bound">A</a>
|
||
<a id="4588" href="Function.Base.html#4588" class="Bound">A</a> <a id="4590" href="Function.Base.html#4562" class="Function Operator">∋</a> <a id="4592" href="Function.Base.html#4592" class="Bound">x</a> <a id="4594" class="Symbol">=</a> <a id="4596" href="Function.Base.html#4592" class="Bound">x</a>
|
||
|
||
<a id="4599" class="Comment">-- Conversely it is sometimes useful to be able to extract the</a>
|
||
<a id="4662" class="Comment">-- type of a given expression.</a>
|
||
|
||
<a id="typeOf"></a><a id="4694" href="Function.Base.html#4694" class="Function">typeOf</a> <a id="4701" class="Symbol">:</a> <a id="4703" class="Symbol">{</a><a id="4704" href="Function.Base.html#4704" class="Bound">A</a> <a id="4706" class="Symbol">:</a> <a id="4708" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4712" href="Function.Base.html#427" class="Generalizable">a</a><a id="4713" class="Symbol">}</a> <a id="4715" class="Symbol">→</a> <a id="4717" href="Function.Base.html#4704" class="Bound">A</a> <a id="4719" class="Symbol">→</a> <a id="4721" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4725" href="Function.Base.html#427" class="Generalizable">a</a>
|
||
<a id="4727" href="Function.Base.html#4694" class="Function">typeOf</a> <a id="4734" class="Symbol">{</a><a id="4735" class="Argument">A</a> <a id="4737" class="Symbol">=</a> <a id="4739" href="Function.Base.html#4739" class="Bound">A</a><a id="4740" class="Symbol">}</a> <a id="4742" class="Symbol">_</a> <a id="4744" class="Symbol">=</a> <a id="4746" href="Function.Base.html#4739" class="Bound">A</a>
|
||
|
||
<a id="4749" class="Comment">-- Construct an element of the given type by instance search.</a>
|
||
|
||
<a id="it"></a><a id="4812" href="Function.Base.html#4812" class="Function">it</a> <a id="4815" class="Symbol">:</a> <a id="4817" class="Symbol">{</a><a id="4818" href="Function.Base.html#4818" class="Bound">A</a> <a id="4820" class="Symbol">:</a> <a id="4822" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4826" href="Function.Base.html#427" class="Generalizable">a</a><a id="4827" class="Symbol">}</a> <a id="4829" class="Symbol">→</a> <a id="4831" class="Symbol">{{</a><a id="4833" href="Function.Base.html#4818" class="Bound">A</a><a id="4834" class="Symbol">}}</a> <a id="4837" class="Symbol">→</a> <a id="4839" href="Function.Base.html#4818" class="Bound">A</a>
|
||
<a id="4841" href="Function.Base.html#4812" class="Function">it</a> <a id="4844" class="Symbol">{{</a><a id="4846" href="Function.Base.html#4846" class="Bound">x</a><a id="4847" class="Symbol">}}</a> <a id="4850" class="Symbol">=</a> <a id="4852" href="Function.Base.html#4846" class="Bound">x</a>
|
||
|
||
<a id="4855" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="4928" class="Comment">-- Composition of a binary function with other functions</a>
|
||
|
||
<a id="4986" class="Keyword">infixr</a> <a id="4993" class="Number">0</a> <a id="4995" href="Function.Base.html#5115" class="Function Operator">_-⟪_⟫-_</a> <a id="5003" href="Function.Base.html#5889" class="Function Operator">_-⟨_⟫-_</a>
|
||
<a id="5011" class="Keyword">infixl</a> <a id="5018" class="Number">0</a> <a id="5020" href="Function.Base.html#5743" class="Function Operator">_-⟪_⟩-_</a>
|
||
<a id="5028" class="Keyword">infixr</a> <a id="5035" class="Number">1</a> <a id="5037" href="Function.Base.html#6015" class="Function Operator">_-⟨_⟩-_</a> <a id="5045" href="Function.Base.html#5382" class="Function Operator">∣_⟫-_</a> <a id="5051" href="Function.Base.html#5621" class="Function Operator">∣_⟩-_</a>
|
||
<a id="5057" class="Keyword">infixl</a> <a id="5064" class="Number">1</a> <a id="5066" href="Function.Base.html#6285" class="Function Operator">_on_</a> <a id="5071" href="Function.Base.html#6168" class="Function Operator">_on₂_</a> <a id="5077" href="Function.Base.html#5259" class="Function Operator">_-⟪_∣</a> <a id="5083" href="Function.Base.html#5502" class="Function Operator">_-⟨_∣</a>
|
||
|
||
<a id="5090" class="Comment">-- Two binary functions</a>
|
||
|
||
<a id="_-⟪_⟫-_"></a><a id="5115" href="Function.Base.html#5115" class="Function Operator">_-⟪_⟫-_</a> <a id="5123" class="Symbol">:</a> <a id="5125" class="Symbol">(</a><a id="5126" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5128" class="Symbol">→</a> <a id="5130" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5132" class="Symbol">→</a> <a id="5134" href="Function.Base.html#477" class="Generalizable">C</a><a id="5135" class="Symbol">)</a> <a id="5137" class="Symbol">→</a> <a id="5139" class="Symbol">(</a><a id="5140" href="Function.Base.html#477" class="Generalizable">C</a> <a id="5142" class="Symbol">→</a> <a id="5144" href="Function.Base.html#491" class="Generalizable">D</a> <a id="5146" class="Symbol">→</a> <a id="5148" href="Function.Base.html#505" class="Generalizable">E</a><a id="5149" class="Symbol">)</a> <a id="5151" class="Symbol">→</a> <a id="5153" class="Symbol">(</a><a id="5154" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5156" class="Symbol">→</a> <a id="5158" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5160" class="Symbol">→</a> <a id="5162" href="Function.Base.html#491" class="Generalizable">D</a><a id="5163" class="Symbol">)</a> <a id="5165" class="Symbol">→</a> <a id="5167" class="Symbol">(</a><a id="5168" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5170" class="Symbol">→</a> <a id="5172" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5174" class="Symbol">→</a> <a id="5176" href="Function.Base.html#505" class="Generalizable">E</a><a id="5177" class="Symbol">)</a>
|
||
<a id="5179" href="Function.Base.html#5179" class="Bound">f</a> <a id="5181" href="Function.Base.html#5115" class="Function Operator">-⟪</a> <a id="5184" href="Function.Base.html#5184" class="Bound Operator">_*_</a> <a id="5188" href="Function.Base.html#5115" class="Function Operator">⟫-</a> <a id="5191" href="Function.Base.html#5191" class="Bound">g</a> <a id="5193" class="Symbol">=</a> <a id="5195" class="Symbol">λ</a> <a id="5197" href="Function.Base.html#5197" class="Bound">x</a> <a id="5199" href="Function.Base.html#5199" class="Bound">y</a> <a id="5201" class="Symbol">→</a> <a id="5203" href="Function.Base.html#5179" class="Bound">f</a> <a id="5205" href="Function.Base.html#5197" class="Bound">x</a> <a id="5207" href="Function.Base.html#5199" class="Bound">y</a> <a id="5209" href="Function.Base.html#5184" class="Bound Operator">*</a> <a id="5211" href="Function.Base.html#5191" class="Bound">g</a> <a id="5213" href="Function.Base.html#5197" class="Bound">x</a> <a id="5215" href="Function.Base.html#5199" class="Bound">y</a>
|
||
|
||
<a id="5218" class="Comment">-- A single binary function on the left</a>
|
||
|
||
<a id="_-⟪_∣"></a><a id="5259" href="Function.Base.html#5259" class="Function Operator">_-⟪_∣</a> <a id="5265" class="Symbol">:</a> <a id="5267" class="Symbol">(</a><a id="5268" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5270" class="Symbol">→</a> <a id="5272" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5274" class="Symbol">→</a> <a id="5276" href="Function.Base.html#477" class="Generalizable">C</a><a id="5277" class="Symbol">)</a> <a id="5279" class="Symbol">→</a> <a id="5281" class="Symbol">(</a><a id="5282" href="Function.Base.html#477" class="Generalizable">C</a> <a id="5284" class="Symbol">→</a> <a id="5286" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5288" class="Symbol">→</a> <a id="5290" href="Function.Base.html#491" class="Generalizable">D</a><a id="5291" class="Symbol">)</a> <a id="5293" class="Symbol">→</a> <a id="5295" class="Symbol">(</a><a id="5296" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5298" class="Symbol">→</a> <a id="5300" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5302" class="Symbol">→</a> <a id="5304" href="Function.Base.html#491" class="Generalizable">D</a><a id="5305" class="Symbol">)</a>
|
||
<a id="5307" href="Function.Base.html#5307" class="Bound">f</a> <a id="5309" href="Function.Base.html#5259" class="Function Operator">-⟪</a> <a id="5312" href="Function.Base.html#5312" class="Bound Operator">_*_</a> <a id="5316" href="Function.Base.html#5259" class="Function Operator">∣</a> <a id="5318" class="Symbol">=</a> <a id="5320" href="Function.Base.html#5307" class="Bound">f</a> <a id="5322" href="Function.Base.html#5115" class="Function Operator">-⟪</a> <a id="5325" href="Function.Base.html#5312" class="Bound Operator">_*_</a> <a id="5329" href="Function.Base.html#5115" class="Function Operator">⟫-</a> <a id="5332" href="Function.Base.html#673" class="Function">constᵣ</a>
|
||
|
||
<a id="5340" class="Comment">-- A single binary function on the right</a>
|
||
|
||
<a id="∣_⟫-_"></a><a id="5382" href="Function.Base.html#5382" class="Function Operator">∣_⟫-_</a> <a id="5388" class="Symbol">:</a> <a id="5390" class="Symbol">(</a><a id="5391" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5393" class="Symbol">→</a> <a id="5395" href="Function.Base.html#477" class="Generalizable">C</a> <a id="5397" class="Symbol">→</a> <a id="5399" href="Function.Base.html#491" class="Generalizable">D</a><a id="5400" class="Symbol">)</a> <a id="5402" class="Symbol">→</a> <a id="5404" class="Symbol">(</a><a id="5405" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5407" class="Symbol">→</a> <a id="5409" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5411" class="Symbol">→</a> <a id="5413" href="Function.Base.html#477" class="Generalizable">C</a><a id="5414" class="Symbol">)</a> <a id="5416" class="Symbol">→</a> <a id="5418" class="Symbol">(</a><a id="5419" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5421" class="Symbol">→</a> <a id="5423" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5425" class="Symbol">→</a> <a id="5427" href="Function.Base.html#491" class="Generalizable">D</a><a id="5428" class="Symbol">)</a>
|
||
<a id="5430" href="Function.Base.html#5382" class="Function Operator">∣</a> <a id="5432" href="Function.Base.html#5432" class="Bound Operator">_*_</a> <a id="5436" href="Function.Base.html#5382" class="Function Operator">⟫-</a> <a id="5439" href="Function.Base.html#5439" class="Bound">g</a> <a id="5441" class="Symbol">=</a> <a id="5443" href="Function.Base.html#636" class="Function">const</a> <a id="5449" href="Function.Base.html#5115" class="Function Operator">-⟪</a> <a id="5452" href="Function.Base.html#5432" class="Bound Operator">_*_</a> <a id="5456" href="Function.Base.html#5115" class="Function Operator">⟫-</a> <a id="5459" href="Function.Base.html#5439" class="Bound">g</a>
|
||
|
||
<a id="5462" class="Comment">-- A single unary function on the left</a>
|
||
|
||
<a id="_-⟨_∣"></a><a id="5502" href="Function.Base.html#5502" class="Function Operator">_-⟨_∣</a> <a id="5508" class="Symbol">:</a> <a id="5510" class="Symbol">(</a><a id="5511" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5513" class="Symbol">→</a> <a id="5515" href="Function.Base.html#477" class="Generalizable">C</a><a id="5516" class="Symbol">)</a> <a id="5518" class="Symbol">→</a> <a id="5520" class="Symbol">(</a><a id="5521" href="Function.Base.html#477" class="Generalizable">C</a> <a id="5523" class="Symbol">→</a> <a id="5525" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5527" class="Symbol">→</a> <a id="5529" href="Function.Base.html#491" class="Generalizable">D</a><a id="5530" class="Symbol">)</a> <a id="5532" class="Symbol">→</a> <a id="5534" class="Symbol">(</a><a id="5535" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5537" class="Symbol">→</a> <a id="5539" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5541" class="Symbol">→</a> <a id="5543" href="Function.Base.html#491" class="Generalizable">D</a><a id="5544" class="Symbol">)</a>
|
||
<a id="5546" href="Function.Base.html#5546" class="Bound">f</a> <a id="5548" href="Function.Base.html#5502" class="Function Operator">-⟨</a> <a id="5551" href="Function.Base.html#5551" class="Bound Operator">_*_</a> <a id="5555" href="Function.Base.html#5502" class="Function Operator">∣</a> <a id="5557" class="Symbol">=</a> <a id="5559" href="Function.Base.html#5546" class="Bound">f</a> <a id="5561" href="Function.Base.html#1219" class="Function Operator">∘₂</a> <a id="5564" href="Function.Base.html#636" class="Function">const</a> <a id="5570" href="Function.Base.html#5259" class="Function Operator">-⟪</a> <a id="5573" href="Function.Base.html#5551" class="Bound Operator">_*_</a> <a id="5577" href="Function.Base.html#5259" class="Function Operator">∣</a>
|
||
|
||
<a id="5580" class="Comment">-- A single unary function on the right</a>
|
||
|
||
<a id="∣_⟩-_"></a><a id="5621" href="Function.Base.html#5621" class="Function Operator">∣_⟩-_</a> <a id="5627" class="Symbol">:</a> <a id="5629" class="Symbol">(</a><a id="5630" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5632" class="Symbol">→</a> <a id="5634" href="Function.Base.html#477" class="Generalizable">C</a> <a id="5636" class="Symbol">→</a> <a id="5638" href="Function.Base.html#491" class="Generalizable">D</a><a id="5639" class="Symbol">)</a> <a id="5641" class="Symbol">→</a> <a id="5643" class="Symbol">(</a><a id="5644" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5646" class="Symbol">→</a> <a id="5648" href="Function.Base.html#477" class="Generalizable">C</a><a id="5649" class="Symbol">)</a> <a id="5651" class="Symbol">→</a> <a id="5653" class="Symbol">(</a><a id="5654" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5656" class="Symbol">→</a> <a id="5658" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5660" class="Symbol">→</a> <a id="5662" href="Function.Base.html#491" class="Generalizable">D</a><a id="5663" class="Symbol">)</a>
|
||
<a id="5665" href="Function.Base.html#5621" class="Function Operator">∣</a> <a id="5667" href="Function.Base.html#5667" class="Bound Operator">_*_</a> <a id="5671" href="Function.Base.html#5621" class="Function Operator">⟩-</a> <a id="5674" href="Function.Base.html#5674" class="Bound">g</a> <a id="5676" class="Symbol">=</a> <a id="5678" href="Function.Base.html#5382" class="Function Operator">∣</a> <a id="5680" href="Function.Base.html#5667" class="Bound Operator">_*_</a> <a id="5684" href="Function.Base.html#5382" class="Function Operator">⟫-</a> <a id="5687" href="Function.Base.html#5674" class="Bound">g</a> <a id="5689" href="Function.Base.html#1219" class="Function Operator">∘₂</a> <a id="5692" href="Function.Base.html#673" class="Function">constᵣ</a>
|
||
|
||
<a id="5700" class="Comment">-- A binary function and a unary function</a>
|
||
|
||
<a id="_-⟪_⟩-_"></a><a id="5743" href="Function.Base.html#5743" class="Function Operator">_-⟪_⟩-_</a> <a id="5751" class="Symbol">:</a> <a id="5753" class="Symbol">(</a><a id="5754" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5756" class="Symbol">→</a> <a id="5758" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5760" class="Symbol">→</a> <a id="5762" href="Function.Base.html#477" class="Generalizable">C</a><a id="5763" class="Symbol">)</a> <a id="5765" class="Symbol">→</a> <a id="5767" class="Symbol">(</a><a id="5768" href="Function.Base.html#477" class="Generalizable">C</a> <a id="5770" class="Symbol">→</a> <a id="5772" href="Function.Base.html#491" class="Generalizable">D</a> <a id="5774" class="Symbol">→</a> <a id="5776" href="Function.Base.html#505" class="Generalizable">E</a><a id="5777" class="Symbol">)</a> <a id="5779" class="Symbol">→</a> <a id="5781" class="Symbol">(</a><a id="5782" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5784" class="Symbol">→</a> <a id="5786" href="Function.Base.html#491" class="Generalizable">D</a><a id="5787" class="Symbol">)</a> <a id="5789" class="Symbol">→</a> <a id="5791" class="Symbol">(</a><a id="5792" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5794" class="Symbol">→</a> <a id="5796" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5798" class="Symbol">→</a> <a id="5800" href="Function.Base.html#505" class="Generalizable">E</a><a id="5801" class="Symbol">)</a>
|
||
<a id="5803" href="Function.Base.html#5803" class="Bound">f</a> <a id="5805" href="Function.Base.html#5743" class="Function Operator">-⟪</a> <a id="5808" href="Function.Base.html#5808" class="Bound Operator">_*_</a> <a id="5812" href="Function.Base.html#5743" class="Function Operator">⟩-</a> <a id="5815" href="Function.Base.html#5815" class="Bound">g</a> <a id="5817" class="Symbol">=</a> <a id="5819" href="Function.Base.html#5803" class="Bound">f</a> <a id="5821" href="Function.Base.html#5115" class="Function Operator">-⟪</a> <a id="5824" href="Function.Base.html#5808" class="Bound Operator">_*_</a> <a id="5828" href="Function.Base.html#5115" class="Function Operator">⟫-</a> <a id="5831" href="Function.Base.html#5621" class="Function Operator">∣</a> <a id="5833" href="Function.Base.html#673" class="Function">constᵣ</a> <a id="5840" href="Function.Base.html#5621" class="Function Operator">⟩-</a> <a id="5843" href="Function.Base.html#5815" class="Bound">g</a>
|
||
|
||
<a id="5846" class="Comment">-- A unary function and a binary function</a>
|
||
|
||
<a id="_-⟨_⟫-_"></a><a id="5889" href="Function.Base.html#5889" class="Function Operator">_-⟨_⟫-_</a> <a id="5897" class="Symbol">:</a> <a id="5899" class="Symbol">(</a><a id="5900" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5902" class="Symbol">→</a> <a id="5904" href="Function.Base.html#477" class="Generalizable">C</a><a id="5905" class="Symbol">)</a> <a id="5907" class="Symbol">→</a> <a id="5909" class="Symbol">(</a><a id="5910" href="Function.Base.html#477" class="Generalizable">C</a> <a id="5912" class="Symbol">→</a> <a id="5914" href="Function.Base.html#491" class="Generalizable">D</a> <a id="5916" class="Symbol">→</a> <a id="5918" href="Function.Base.html#505" class="Generalizable">E</a><a id="5919" class="Symbol">)</a> <a id="5921" class="Symbol">→</a> <a id="5923" class="Symbol">(</a><a id="5924" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5926" class="Symbol">→</a> <a id="5928" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5930" class="Symbol">→</a> <a id="5932" href="Function.Base.html#491" class="Generalizable">D</a><a id="5933" class="Symbol">)</a> <a id="5935" class="Symbol">→</a> <a id="5937" class="Symbol">(</a><a id="5938" href="Function.Base.html#449" class="Generalizable">A</a> <a id="5940" class="Symbol">→</a> <a id="5942" href="Function.Base.html#463" class="Generalizable">B</a> <a id="5944" class="Symbol">→</a> <a id="5946" href="Function.Base.html#505" class="Generalizable">E</a><a id="5947" class="Symbol">)</a>
|
||
<a id="5949" href="Function.Base.html#5949" class="Bound">f</a> <a id="5951" href="Function.Base.html#5889" class="Function Operator">-⟨</a> <a id="5954" href="Function.Base.html#5954" class="Bound Operator">_*_</a> <a id="5958" href="Function.Base.html#5889" class="Function Operator">⟫-</a> <a id="5961" href="Function.Base.html#5961" class="Bound">g</a> <a id="5963" class="Symbol">=</a> <a id="5965" href="Function.Base.html#5949" class="Bound">f</a> <a id="5967" href="Function.Base.html#5502" class="Function Operator">-⟨</a> <a id="5970" href="Function.Base.html#636" class="Function">const</a> <a id="5976" href="Function.Base.html#5502" class="Function Operator">∣</a> <a id="5978" href="Function.Base.html#5115" class="Function Operator">-⟪</a> <a id="5981" href="Function.Base.html#5954" class="Bound Operator">_*_</a> <a id="5985" href="Function.Base.html#5115" class="Function Operator">⟫-</a> <a id="5988" href="Function.Base.html#5961" class="Bound">g</a>
|
||
|
||
<a id="5991" class="Comment">-- Two unary functions</a>
|
||
|
||
<a id="_-⟨_⟩-_"></a><a id="6015" href="Function.Base.html#6015" class="Function Operator">_-⟨_⟩-_</a> <a id="6023" class="Symbol">:</a> <a id="6025" class="Symbol">(</a><a id="6026" href="Function.Base.html#449" class="Generalizable">A</a> <a id="6028" class="Symbol">→</a> <a id="6030" href="Function.Base.html#477" class="Generalizable">C</a><a id="6031" class="Symbol">)</a> <a id="6033" class="Symbol">→</a> <a id="6035" class="Symbol">(</a><a id="6036" href="Function.Base.html#477" class="Generalizable">C</a> <a id="6038" class="Symbol">→</a> <a id="6040" href="Function.Base.html#491" class="Generalizable">D</a> <a id="6042" class="Symbol">→</a> <a id="6044" href="Function.Base.html#505" class="Generalizable">E</a><a id="6045" class="Symbol">)</a> <a id="6047" class="Symbol">→</a> <a id="6049" class="Symbol">(</a><a id="6050" href="Function.Base.html#463" class="Generalizable">B</a> <a id="6052" class="Symbol">→</a> <a id="6054" href="Function.Base.html#491" class="Generalizable">D</a><a id="6055" class="Symbol">)</a> <a id="6057" class="Symbol">→</a> <a id="6059" class="Symbol">(</a><a id="6060" href="Function.Base.html#449" class="Generalizable">A</a> <a id="6062" class="Symbol">→</a> <a id="6064" href="Function.Base.html#463" class="Generalizable">B</a> <a id="6066" class="Symbol">→</a> <a id="6068" href="Function.Base.html#505" class="Generalizable">E</a><a id="6069" class="Symbol">)</a>
|
||
<a id="6071" href="Function.Base.html#6071" class="Bound">f</a> <a id="6073" href="Function.Base.html#6015" class="Function Operator">-⟨</a> <a id="6076" href="Function.Base.html#6076" class="Bound Operator">_*_</a> <a id="6080" href="Function.Base.html#6015" class="Function Operator">⟩-</a> <a id="6083" href="Function.Base.html#6083" class="Bound">g</a> <a id="6085" class="Symbol">=</a> <a id="6087" href="Function.Base.html#6071" class="Bound">f</a> <a id="6089" href="Function.Base.html#5502" class="Function Operator">-⟨</a> <a id="6092" href="Function.Base.html#636" class="Function">const</a> <a id="6098" href="Function.Base.html#5502" class="Function Operator">∣</a> <a id="6100" href="Function.Base.html#5115" class="Function Operator">-⟪</a> <a id="6103" href="Function.Base.html#6076" class="Bound Operator">_*_</a> <a id="6107" href="Function.Base.html#5115" class="Function Operator">⟫-</a> <a id="6110" href="Function.Base.html#5621" class="Function Operator">∣</a> <a id="6112" href="Function.Base.html#673" class="Function">constᵣ</a> <a id="6119" href="Function.Base.html#5621" class="Function Operator">⟩-</a> <a id="6122" href="Function.Base.html#6083" class="Bound">g</a>
|
||
|
||
<a id="6125" class="Comment">-- A single binary function on both sides</a>
|
||
|
||
<a id="_on₂_"></a><a id="6168" href="Function.Base.html#6168" class="Function Operator">_on₂_</a> <a id="6174" class="Symbol">:</a> <a id="6176" class="Symbol">(</a><a id="6177" href="Function.Base.html#477" class="Generalizable">C</a> <a id="6179" class="Symbol">→</a> <a id="6181" href="Function.Base.html#477" class="Generalizable">C</a> <a id="6183" class="Symbol">→</a> <a id="6185" href="Function.Base.html#491" class="Generalizable">D</a><a id="6186" class="Symbol">)</a> <a id="6188" class="Symbol">→</a> <a id="6190" class="Symbol">(</a><a id="6191" href="Function.Base.html#449" class="Generalizable">A</a> <a id="6193" class="Symbol">→</a> <a id="6195" href="Function.Base.html#463" class="Generalizable">B</a> <a id="6197" class="Symbol">→</a> <a id="6199" href="Function.Base.html#477" class="Generalizable">C</a><a id="6200" class="Symbol">)</a> <a id="6202" class="Symbol">→</a> <a id="6204" class="Symbol">(</a><a id="6205" href="Function.Base.html#449" class="Generalizable">A</a> <a id="6207" class="Symbol">→</a> <a id="6209" href="Function.Base.html#463" class="Generalizable">B</a> <a id="6211" class="Symbol">→</a> <a id="6213" href="Function.Base.html#491" class="Generalizable">D</a><a id="6214" class="Symbol">)</a>
|
||
<a id="6216" href="Function.Base.html#6216" class="Bound Operator">_*_</a> <a id="6220" href="Function.Base.html#6168" class="Function Operator">on₂</a> <a id="6224" href="Function.Base.html#6224" class="Bound">f</a> <a id="6226" class="Symbol">=</a> <a id="6228" href="Function.Base.html#6224" class="Bound">f</a> <a id="6230" href="Function.Base.html#5115" class="Function Operator">-⟪</a> <a id="6233" href="Function.Base.html#6216" class="Bound Operator">_*_</a> <a id="6237" href="Function.Base.html#5115" class="Function Operator">⟫-</a> <a id="6240" href="Function.Base.html#6224" class="Bound">f</a>
|
||
|
||
<a id="6243" class="Comment">-- A single unary function on both sides</a>
|
||
|
||
<a id="_on_"></a><a id="6285" href="Function.Base.html#6285" class="Function Operator">_on_</a> <a id="6290" class="Symbol">:</a> <a id="6292" class="Symbol">(</a><a id="6293" href="Function.Base.html#463" class="Generalizable">B</a> <a id="6295" class="Symbol">→</a> <a id="6297" href="Function.Base.html#463" class="Generalizable">B</a> <a id="6299" class="Symbol">→</a> <a id="6301" href="Function.Base.html#477" class="Generalizable">C</a><a id="6302" class="Symbol">)</a> <a id="6304" class="Symbol">→</a> <a id="6306" class="Symbol">(</a><a id="6307" href="Function.Base.html#449" class="Generalizable">A</a> <a id="6309" class="Symbol">→</a> <a id="6311" href="Function.Base.html#463" class="Generalizable">B</a><a id="6312" class="Symbol">)</a> <a id="6314" class="Symbol">→</a> <a id="6316" class="Symbol">(</a><a id="6317" href="Function.Base.html#449" class="Generalizable">A</a> <a id="6319" class="Symbol">→</a> <a id="6321" href="Function.Base.html#449" class="Generalizable">A</a> <a id="6323" class="Symbol">→</a> <a id="6325" href="Function.Base.html#477" class="Generalizable">C</a><a id="6326" class="Symbol">)</a>
|
||
<a id="6328" href="Function.Base.html#6328" class="Bound Operator">_*_</a> <a id="6332" href="Function.Base.html#6285" class="Function Operator">on</a> <a id="6335" href="Function.Base.html#6335" class="Bound">f</a> <a id="6337" class="Symbol">=</a> <a id="6339" href="Function.Base.html#6335" class="Bound">f</a> <a id="6341" href="Function.Base.html#6015" class="Function Operator">-⟨</a> <a id="6344" href="Function.Base.html#6328" class="Bound Operator">_*_</a> <a id="6348" href="Function.Base.html#6015" class="Function Operator">⟩-</a> <a id="6351" href="Function.Base.html#6335" class="Bound">f</a>
|
||
|
||
<a id="_-[_]-_"></a><a id="6354" href="Function.Base.html#6354" class="Function Operator">_-[_]-_</a> <a id="6362" class="Symbol">=</a> <a id="6364" href="Function.Base.html#5115" class="Function Operator">_-⟪_⟫-_</a>
|
||
<a id="6372" class="Symbol">{-#</a> <a id="6376" class="Keyword">WARNING_ON_USAGE</a> <a id="6393" class="Pragma">_-[_]-_</a>
|
||
<a id="6401" class="String">"Warning: Function._-[_]-_ was deprecated in v1.4.
|
||
Please use _-⟪_⟫-_ instead."</a>
|
||
<a id="6481" class="Symbol">#-}</a>
|
||
</pre></body></html> |