agda-stdlib-doc 0.14-1 / usr / share / doc / agda-stdlib-doc / html / Data.Graph.Acyclic.html

This file is indexed.

/usr/share/doc/agda-stdlib-doc/html/Data.Graph.Acyclic.html is in agda-stdlib-doc 0.14-1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Data.Graph.Acyclic</title><link rel="stylesheet" href="Agda.css"></head><body><pre><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">-- Directed acyclic multigraphs</a>
<a id="138" class="Comment">------------------------------------------------------------------------</a>

<a id="212" class="Comment">-- A representation of DAGs, based on the idea underlying Martin</a>
<a id="277" class="Comment">-- Erwig&#39;s FGL. Note that this representation does not aim to be</a>
<a id="342" class="Comment">-- efficient.</a>

<a id="357" class="Keyword">module</a> <a id="364" href="Data.Graph.Acyclic.html" class="Module">Data.Graph.Acyclic</a> <a id="383" class="Keyword">where</a>

<a id="390" class="Keyword">open</a> <a id="395" class="Keyword">import</a> <a id="402" href="Data.Nat.Base.html" class="Module">Data.Nat.Base</a> <a id="416" class="Symbol">as</a> <a id="419" class="Module">Nat</a> <a id="423" class="Keyword">using</a> <a id="429" class="Symbol">(</a><a id="430" href="Agda.Builtin.Nat.html#Nat" class="Datatype">ℕ</a><a id="431" class="Symbol">;</a> <a id="433" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a><a id="437" class="Symbol">;</a> <a id="439" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a><a id="442" class="Symbol">;</a> <a id="444" href="Data.Nat.Base.html#_%3C%E2%80%B2_" class="Function Operator">_&lt;′_</a><a id="448" class="Symbol">)</a>
<a id="450" class="Keyword">import</a> <a id="457" href="Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="477" class="Symbol">as</a> <a id="480" class="Module">Nat</a>
<a id="484" class="Keyword">open</a> <a id="489" class="Keyword">import</a> <a id="496" href="Data.Fin.html" class="Module">Data.Fin</a> <a id="505" class="Symbol">as</a> <a id="508" class="Module">Fin</a>
  <a id="514" class="Keyword">using</a> <a id="520" class="Symbol">(</a><a id="521" href="Data.Fin.html#Fin" class="Datatype">Fin</a><a id="524" class="Symbol">;</a> <a id="526" href="Data.Fin.html#Fin%E2%80%B2" class="Function">Fin′</a><a id="530" class="Symbol">;</a> <a id="532" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a><a id="536" class="Symbol">;</a> <a id="538" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a><a id="541" class="Symbol">;</a> <a id="543" href="Data.Fin.html#%23_" class="Function Operator">#_</a><a id="545" class="Symbol">;</a> <a id="547" href="Data.Fin.html#to%E2%84%95" class="Function">toℕ</a><a id="550" class="Symbol">)</a> <a id="552" class="Keyword">renaming</a> <a id="561" class="Symbol">(</a><a id="562" href="Data.Fin.html#_%E2%84%95-%E2%84%95_" class="Function Operator">_ℕ-ℕ_</a> <a id="568" class="Symbol">to</a> <a id="571" href="Data.Fin.html#_%E2%84%95-%E2%84%95_" class="Function Operator">_-_</a><a id="574" class="Symbol">)</a>
<a id="576" class="Keyword">open</a> <a id="581" class="Keyword">import</a> <a id="588" href="Data.Fin.Properties.html" class="Module">Data.Fin.Properties</a> <a id="608" class="Symbol">as</a> <a id="611" class="Module">FP</a> <a id="614" class="Keyword">using</a> <a id="620" class="Symbol">(</a><a id="621" href="Data.Fin.Properties.html#_%E2%89%9F_" class="Function Operator">_≟_</a><a id="624" class="Symbol">)</a>
<a id="626" class="Keyword">open</a> <a id="631" class="Keyword">import</a> <a id="638" href="Data.Product.html" class="Module">Data.Product</a> <a id="651" class="Symbol">as</a> <a id="654" class="Module">Prod</a> <a id="659" class="Keyword">using</a> <a id="665" class="Symbol">(</a><a id="666" href="Data.Product.html#%E2%88%83" class="Function">∃</a><a id="667" class="Symbol">;</a> <a id="669" href="Data.Product.html#_%C3%97_" class="Function Operator">_×_</a><a id="672" class="Symbol">;</a> <a id="674" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">_,_</a><a id="677" class="Symbol">)</a>
<a id="679" class="Keyword">open</a> <a id="684" class="Keyword">import</a> <a id="691" href="Data.Maybe.Base.html" class="Module">Data.Maybe.Base</a> <a id="707" class="Keyword">using</a> <a id="713" class="Symbol">(</a><a id="714" href="Data.Maybe.Base.html#Maybe" class="Datatype">Maybe</a><a id="719" class="Symbol">;</a> <a id="721" href="Data.Maybe.Base.html#Maybe.nothing" class="InductiveConstructor">nothing</a><a id="728" class="Symbol">;</a> <a id="730" href="Data.Maybe.Base.html#Maybe.just" class="InductiveConstructor">just</a><a id="734" class="Symbol">)</a>
<a id="736" class="Keyword">open</a> <a id="741" class="Keyword">import</a> <a id="748" href="Data.Empty.html" class="Module">Data.Empty</a>
<a id="759" class="Keyword">open</a> <a id="764" class="Keyword">import</a> <a id="771" href="Data.Unit.Base.html" class="Module">Data.Unit.Base</a> <a id="786" class="Keyword">using</a> <a id="792" class="Symbol">(</a><a id="793" href="Agda.Builtin.Unit.html#%E2%8A%A4" class="Record">⊤</a><a id="794" class="Symbol">;</a> <a id="796" href="Agda.Builtin.Unit.html#%E2%8A%A4.tt" class="InductiveConstructor">tt</a><a id="798" class="Symbol">)</a>
<a id="800" class="Keyword">open</a> <a id="805" class="Keyword">import</a> <a id="812" href="Data.Vec.html" class="Module">Data.Vec</a> <a id="821" class="Symbol">as</a> <a id="824" class="Module">Vec</a> <a id="828" class="Keyword">using</a> <a id="834" class="Symbol">(</a><a id="835" href="Data.Vec.html#Vec" class="Datatype">Vec</a><a id="838" class="Symbol">;</a> <a id="840" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a><a id="842" class="Symbol">;</a> <a id="844" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">_∷_</a><a id="847" class="Symbol">)</a>
<a id="849" class="Keyword">open</a> <a id="854" class="Keyword">import</a> <a id="861" href="Data.List.Base.html" class="Module">Data.List.Base</a> <a id="876" class="Symbol">as</a> <a id="879" class="Module">List</a> <a id="884" class="Keyword">using</a> <a id="890" class="Symbol">(</a><a id="891" href="Agda.Builtin.List.html#List" class="Datatype">List</a><a id="895" class="Symbol">;</a> <a id="897" href="Data.List.Base.html#InitLast.%5B%5D" class="InductiveConstructor">[]</a><a id="899" class="Symbol">;</a> <a id="901" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">_∷_</a><a id="904" class="Symbol">)</a>
<a id="906" class="Keyword">open</a> <a id="911" class="Keyword">import</a> <a id="918" href="Function.html" class="Module">Function</a>
<a id="927" class="Keyword">open</a> <a id="932" class="Keyword">import</a> <a id="939" href="Induction.Nat.html" class="Module">Induction.Nat</a> <a id="953" class="Keyword">using</a> <a id="959" class="Symbol">(</a><a id="960" href="Induction.WellFounded.html#1751" class="Function">&lt;′-rec</a><a id="966" class="Symbol">;</a> <a id="968" href="Induction.Nat.html#%3C%E2%80%B2-Rec" class="Function">&lt;′-Rec</a><a id="974" class="Symbol">)</a>
<a id="976" class="Keyword">open</a> <a id="981" class="Keyword">import</a> <a id="988" href="Relation.Nullary.html" class="Module">Relation.Nullary</a>
<a id="1005" class="Keyword">open</a> <a id="1010" class="Keyword">import</a> <a id="1017" href="Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="1055" class="Symbol">as</a> <a id="1058" class="Module">P</a> <a id="1060" class="Keyword">using</a> <a id="1066" class="Symbol">(</a><a id="1067" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">_≡_</a><a id="1070" class="Symbol">)</a>

<a id="1073" class="Comment">------------------------------------------------------------------------</a>
<a id="1146" class="Comment">-- A lemma</a>

<a id="1158" class="Keyword">private</a>

  <a id="lemma" href="Data.Graph.Acyclic.html#lemma" class="Function">lemma</a> <a id="1175" class="Symbol">:</a> <a id="1177" class="Symbol">∀</a> <a id="1179" href="Data.Graph.Acyclic.html#1179" class="Bound">n</a> <a id="1181" class="Symbol">(</a><a id="1182" href="Data.Graph.Acyclic.html#1182" class="Bound">i</a> <a id="1184" class="Symbol">:</a> <a id="1186" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1190" href="Data.Graph.Acyclic.html#1179" class="Bound">n</a><a id="1191" class="Symbol">)</a> <a id="1193" class="Symbol">→</a> <a id="1195" href="Data.Graph.Acyclic.html#1179" class="Bound">n</a> <a id="1197" href="Data.Fin.html#_-_" class="Function Operator">-</a> <a id="1199" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="1203" href="Data.Graph.Acyclic.html#1182" class="Bound">i</a> <a id="1205" href="Data.Nat.Base.html#_%3C%E2%80%B2_" class="Function Operator">&lt;′</a> <a id="1208" href="Data.Graph.Acyclic.html#1179" class="Bound">n</a>
  <a id="1212" href="Data.Graph.Acyclic.html#lemma" class="Function">lemma</a> <a id="1218" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a>    <a id="1226" class="Symbol">()</a>
  <a id="1231" href="Data.Graph.Acyclic.html#lemma" class="Function">lemma</a> <a id="1237" class="Symbol">(</a><a id="1238" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="1242" href="Data.Graph.Acyclic.html#1242" class="Bound">n</a><a id="1243" class="Symbol">)</a> <a id="1245" href="Data.Graph.Acyclic.html#1245" class="Bound">i</a>  <a id="1248" class="Symbol">=</a> <a id="1250" href="Data.Nat.Properties.html#%E2%89%A4%E2%87%92%E2%89%A4%E2%80%B2" class="Function">Nat.≤⇒≤′</a> <a id="1259" href="Function.html#_%24_" class="Function Operator">$</a> <a id="1261" href="Data.Nat.Base.html#_%E2%89%A4_.s%E2%89%A4s" class="InductiveConstructor">Nat.s≤s</a> <a id="1269" href="Function.html#_%24_" class="Function Operator">$</a> <a id="1271" href="Data.Fin.Properties.html#n%E2%84%95-%E2%84%95i%E2%89%A4n" class="Function">FP.nℕ-ℕi≤n</a> <a id="1282" href="Data.Graph.Acyclic.html#1242" class="Bound">n</a> <a id="1284" href="Data.Graph.Acyclic.html#1245" class="Bound">i</a>

<a id="1287" class="Comment">------------------------------------------------------------------------</a>
<a id="1360" class="Comment">-- Node contexts</a>

<a id="1378" class="Keyword">record</a> <a id="Context" href="Data.Graph.Acyclic.html#Context" class="Record">Context</a> <a id="1393" class="Symbol">(</a><a id="1394" href="Data.Graph.Acyclic.html#1394" class="Bound">Node</a> <a id="1399" href="Data.Graph.Acyclic.html#1399" class="Bound">Edge</a> <a id="1404" class="Symbol">:</a> <a id="1406" class="PrimitiveType">Set</a><a id="1409" class="Symbol">)</a> <a id="1411" class="Symbol">(</a><a id="1412" href="Data.Graph.Acyclic.html#1412" class="Bound">n</a> <a id="1414" class="Symbol">:</a> <a id="1416" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="1417" class="Symbol">)</a> <a id="1419" class="Symbol">:</a> <a id="1421" class="PrimitiveType">Set</a> <a id="1425" class="Keyword">where</a>
  <a id="1433" class="Keyword">constructor</a> <a id="Context.context" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a>
  <a id="1455" class="Keyword">field</a>
    <a id="Context.label" href="Data.Graph.Acyclic.html#Context.label" class="Field">label</a>      <a id="1476" class="Symbol">:</a> <a id="1478" href="Data.Graph.Acyclic.html#1394" class="Bound">Node</a>
    <a id="Context.successors" href="Data.Graph.Acyclic.html#Context.successors" class="Field">successors</a> <a id="1498" class="Symbol">:</a> <a id="1500" href="Agda.Builtin.List.html#List" class="Datatype">List</a> <a id="1505" class="Symbol">(</a><a id="1506" href="Data.Graph.Acyclic.html#1399" class="Bound">Edge</a> <a id="1511" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="1513" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1517" href="Data.Graph.Acyclic.html#1412" class="Bound">n</a><a id="1518" class="Symbol">)</a>

<a id="1521" class="Keyword">open</a> <a id="1526" href="Data.Graph.Acyclic.html#Context" class="Module">Context</a> <a id="1534" class="Keyword">public</a>

<a id="1542" class="Comment">-- Map for contexts.</a>

<a id="cmap" href="Data.Graph.Acyclic.html#cmap" class="Function">cmap</a> <a id="1569" class="Symbol">:</a> <a id="1571" class="Symbol">∀</a> <a id="1573" class="Symbol">{</a><a id="1574" href="Data.Graph.Acyclic.html#1574" class="Bound">N₁</a> <a id="1577" href="Data.Graph.Acyclic.html#1577" class="Bound">N₂</a> <a id="1580" href="Data.Graph.Acyclic.html#1580" class="Bound">E₁</a> <a id="1583" href="Data.Graph.Acyclic.html#1583" class="Bound">E₂</a> <a id="1586" href="Data.Graph.Acyclic.html#1586" class="Bound">n</a><a id="1587" class="Symbol">}</a> <a id="1589" class="Symbol">→</a>
       <a id="1598" class="Symbol">(</a><a id="1599" href="Data.Graph.Acyclic.html#1574" class="Bound">N₁</a> <a id="1602" class="Symbol">→</a> <a id="1604" href="Data.Graph.Acyclic.html#1577" class="Bound">N₂</a><a id="1606" class="Symbol">)</a> <a id="1608" class="Symbol">→</a> <a id="1610" class="Symbol">(</a><a id="1611" href="Agda.Builtin.List.html#List" class="Datatype">List</a> <a id="1616" class="Symbol">(</a><a id="1617" href="Data.Graph.Acyclic.html#1580" class="Bound">E₁</a> <a id="1620" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="1622" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1626" href="Data.Graph.Acyclic.html#1586" class="Bound">n</a><a id="1627" class="Symbol">)</a> <a id="1629" class="Symbol">→</a> <a id="1631" href="Agda.Builtin.List.html#List" class="Datatype">List</a> <a id="1636" class="Symbol">(</a><a id="1637" href="Data.Graph.Acyclic.html#1583" class="Bound">E₂</a> <a id="1640" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="1642" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1646" href="Data.Graph.Acyclic.html#1586" class="Bound">n</a><a id="1647" class="Symbol">))</a> <a id="1650" class="Symbol">→</a>
       <a id="1659" href="Data.Graph.Acyclic.html#Context" class="Record">Context</a> <a id="1667" href="Data.Graph.Acyclic.html#1574" class="Bound">N₁</a> <a id="1670" href="Data.Graph.Acyclic.html#1580" class="Bound">E₁</a> <a id="1673" href="Data.Graph.Acyclic.html#1586" class="Bound">n</a> <a id="1675" class="Symbol">→</a> <a id="1677" href="Data.Graph.Acyclic.html#Context" class="Record">Context</a> <a id="1685" href="Data.Graph.Acyclic.html#1577" class="Bound">N₂</a> <a id="1688" href="Data.Graph.Acyclic.html#1583" class="Bound">E₂</a> <a id="1691" href="Data.Graph.Acyclic.html#1586" class="Bound">n</a>
<a id="1693" href="Data.Graph.Acyclic.html#cmap" class="Function">cmap</a> <a id="1698" href="Data.Graph.Acyclic.html#1698" class="Bound">f</a> <a id="1700" href="Data.Graph.Acyclic.html#1700" class="Bound">g</a> <a id="1702" href="Data.Graph.Acyclic.html#1702" class="Bound">c</a> <a id="1704" class="Symbol">=</a> <a id="1706" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="1714" class="Symbol">(</a><a id="1715" href="Data.Graph.Acyclic.html#1698" class="Bound">f</a> <a id="1717" class="Symbol">(</a><a id="1718" href="Data.Graph.Acyclic.html#Context.label" class="Field">label</a> <a id="1724" href="Data.Graph.Acyclic.html#1702" class="Bound">c</a><a id="1725" class="Symbol">))</a> <a id="1728" class="Symbol">(</a><a id="1729" href="Data.Graph.Acyclic.html#1700" class="Bound">g</a> <a id="1731" class="Symbol">(</a><a id="1732" href="Data.Graph.Acyclic.html#Context.successors" class="Field">successors</a> <a id="1743" href="Data.Graph.Acyclic.html#1702" class="Bound">c</a><a id="1744" class="Symbol">))</a>

<a id="1748" class="Comment">------------------------------------------------------------------------</a>
<a id="1821" class="Comment">-- Graphs</a>

<a id="1832" class="Keyword">infixr</a> <a id="1839" class="Number">3</a> <a id="1841" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">_&amp;_</a>

<a id="1846" class="Comment">-- The DAGs are indexed on the number of nodes.</a>

<a id="1895" class="Keyword">data</a> <a id="Graph" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="1906" class="Symbol">(</a><a id="1907" href="Data.Graph.Acyclic.html#1907" class="Bound">Node</a> <a id="1912" href="Data.Graph.Acyclic.html#1912" class="Bound">Edge</a> <a id="1917" class="Symbol">:</a> <a id="1919" class="PrimitiveType">Set</a><a id="1922" class="Symbol">)</a> <a id="1924" class="Symbol">:</a> <a id="1926" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="1928" class="Symbol">→</a> <a id="1930" class="PrimitiveType">Set</a> <a id="1934" class="Keyword">where</a>
  <a id="Graph.∅" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>   <a id="1946" class="Symbol">:</a> <a id="1948" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="1954" href="Data.Graph.Acyclic.html#1907" class="Bound">Node</a> <a id="1959" href="Data.Graph.Acyclic.html#1912" class="Bound">Edge</a> <a id="1964" class="Number">0</a>
  <a id="Graph._&amp;_" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">_&amp;_</a> <a id="1972" class="Symbol">:</a> <a id="1974" class="Symbol">∀</a> <a id="1976" class="Symbol">{</a><a id="1977" href="Data.Graph.Acyclic.html#1977" class="Bound">n</a><a id="1978" class="Symbol">}</a> <a id="1980" class="Symbol">(</a><a id="1981" href="Data.Graph.Acyclic.html#1981" class="Bound">c</a> <a id="1983" class="Symbol">:</a> <a id="1985" href="Data.Graph.Acyclic.html#Context" class="Record">Context</a> <a id="1993" href="Data.Graph.Acyclic.html#1907" class="Bound">Node</a> <a id="1998" href="Data.Graph.Acyclic.html#1912" class="Bound">Edge</a> <a id="2003" href="Data.Graph.Acyclic.html#1977" class="Bound">n</a><a id="2004" class="Symbol">)</a> <a id="2006" class="Symbol">(</a><a id="2007" href="Data.Graph.Acyclic.html#2007" class="Bound">g</a> <a id="2009" class="Symbol">:</a> <a id="2011" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="2017" href="Data.Graph.Acyclic.html#1907" class="Bound">Node</a> <a id="2022" href="Data.Graph.Acyclic.html#1912" class="Bound">Edge</a> <a id="2027" href="Data.Graph.Acyclic.html#1977" class="Bound">n</a><a id="2028" class="Symbol">)</a> <a id="2030" class="Symbol">→</a>
        <a id="2040" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="2046" href="Data.Graph.Acyclic.html#1907" class="Bound">Node</a> <a id="2051" href="Data.Graph.Acyclic.html#1912" class="Bound">Edge</a> <a id="2056" class="Symbol">(</a><a id="2057" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="2061" href="Data.Graph.Acyclic.html#1977" class="Bound">n</a><a id="2062" class="Symbol">)</a>

<a id="2065" class="Keyword">private</a>

  <a id="example" href="Data.Graph.Acyclic.html#example" class="Function">example</a> <a id="2084" class="Symbol">:</a> <a id="2086" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="2092" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="2094" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="2096" class="Number">5</a>
  <a id="2100" href="Data.Graph.Acyclic.html#example" class="Function">example</a> <a id="2108" class="Symbol">=</a> <a id="2110" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="2118" class="Number">0</a> <a id="2120" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a> <a id="2123" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a>
            <a id="2137" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="2145" class="Number">1</a> <a id="2147" class="Symbol">((</a><a id="2149" class="Number">10</a> <a id="2152" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="2154" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="2156" class="Number">1</a><a id="2157" class="Symbol">)</a> <a id="2159" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2161" class="Symbol">(</a><a id="2162" class="Number">11</a> <a id="2165" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="2167" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="2169" class="Number">1</a><a id="2170" class="Symbol">)</a> <a id="2172" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2174" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a><a id="2176" class="Symbol">)</a> <a id="2178" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a>
            <a id="2192" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="2200" class="Number">2</a> <a id="2202" class="Symbol">((</a><a id="2204" class="Number">12</a> <a id="2207" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="2209" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="2211" class="Number">0</a><a id="2212" class="Symbol">)</a> <a id="2214" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2216" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a><a id="2218" class="Symbol">)</a> <a id="2220" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a>
            <a id="2234" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="2242" class="Number">3</a> <a id="2244" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a> <a id="2247" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a>
            <a id="2261" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="2269" class="Number">4</a> <a id="2271" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a> <a id="2274" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a>
            <a id="2288" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>

<a id="2291" class="Comment">------------------------------------------------------------------------</a>
<a id="2364" class="Comment">-- Higher-order functions</a>

<a id="2391" class="Comment">-- &quot;Fold right&quot;.</a>

<a id="foldr" href="Data.Graph.Acyclic.html#foldr" class="Function">foldr</a> <a id="2415" class="Symbol">:</a> <a id="2417" class="Symbol">∀</a> <a id="2419" class="Symbol">{</a><a id="2420" href="Data.Graph.Acyclic.html#2420" class="Bound">N</a> <a id="2422" href="Data.Graph.Acyclic.html#2422" class="Bound">E</a> <a id="2424" href="Data.Graph.Acyclic.html#2424" class="Bound">m</a><a id="2425" class="Symbol">}</a> <a id="2427" class="Symbol">(</a><a id="2428" href="Data.Graph.Acyclic.html#2428" class="Bound">T</a> <a id="2430" class="Symbol">:</a> <a id="2432" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="2434" class="Symbol">→</a> <a id="2436" class="PrimitiveType">Set</a><a id="2439" class="Symbol">)</a> <a id="2441" class="Symbol">→</a>
        <a id="2451" class="Symbol">(∀</a> <a id="2454" class="Symbol">{</a><a id="2455" href="Data.Graph.Acyclic.html#2455" class="Bound">n</a><a id="2456" class="Symbol">}</a> <a id="2458" class="Symbol">→</a> <a id="2460" href="Data.Graph.Acyclic.html#Context" class="Record">Context</a> <a id="2468" href="Data.Graph.Acyclic.html#2420" class="Bound">N</a> <a id="2470" href="Data.Graph.Acyclic.html#2422" class="Bound">E</a> <a id="2472" href="Data.Graph.Acyclic.html#2455" class="Bound">n</a> <a id="2474" class="Symbol">→</a> <a id="2476" href="Data.Graph.Acyclic.html#2428" class="Bound">T</a> <a id="2478" href="Data.Graph.Acyclic.html#2455" class="Bound">n</a> <a id="2480" class="Symbol">→</a> <a id="2482" href="Data.Graph.Acyclic.html#2428" class="Bound">T</a> <a id="2484" class="Symbol">(</a><a id="2485" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="2489" href="Data.Graph.Acyclic.html#2455" class="Bound">n</a><a id="2490" class="Symbol">))</a> <a id="2493" class="Symbol">→</a>
        <a id="2503" href="Data.Graph.Acyclic.html#2428" class="Bound">T</a> <a id="2505" class="Number">0</a> <a id="2507" class="Symbol">→</a>
        <a id="2517" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="2523" href="Data.Graph.Acyclic.html#2420" class="Bound">N</a> <a id="2525" href="Data.Graph.Acyclic.html#2422" class="Bound">E</a> <a id="2527" href="Data.Graph.Acyclic.html#2424" class="Bound">m</a> <a id="2529" class="Symbol">→</a> <a id="2531" href="Data.Graph.Acyclic.html#2428" class="Bound">T</a> <a id="2533" href="Data.Graph.Acyclic.html#2424" class="Bound">m</a>
<a id="2535" href="Data.Graph.Acyclic.html#foldr" class="Function">foldr</a> <a id="2541" href="Data.Graph.Acyclic.html#2541" class="Bound">T</a> <a id="2543" href="Data.Graph.Acyclic.html#2543" class="Bound Operator">_∙_</a> <a id="2547" href="Data.Graph.Acyclic.html#2547" class="Bound">x</a> <a id="2549" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>       <a id="2557" class="Symbol">=</a> <a id="2559" href="Data.Graph.Acyclic.html#2547" class="Bound">x</a>
<a id="2561" href="Data.Graph.Acyclic.html#foldr" class="Function">foldr</a> <a id="2567" href="Data.Graph.Acyclic.html#2567" class="Bound">T</a> <a id="2569" href="Data.Graph.Acyclic.html#2569" class="Bound Operator">_∙_</a> <a id="2573" href="Data.Graph.Acyclic.html#2573" class="Bound">x</a> <a id="2575" class="Symbol">(</a><a id="2576" href="Data.Graph.Acyclic.html#2576" class="Bound">c</a> <a id="2578" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="2580" href="Data.Graph.Acyclic.html#2580" class="Bound">g</a><a id="2581" class="Symbol">)</a> <a id="2583" class="Symbol">=</a> <a id="2585" href="Data.Graph.Acyclic.html#2576" class="Bound">c</a> <a id="2587" href="Data.Graph.Acyclic.html#2569" class="Bound Operator">∙</a> <a id="2589" href="Data.Graph.Acyclic.html#foldr" class="Function">foldr</a> <a id="2595" href="Data.Graph.Acyclic.html#2567" class="Bound">T</a> <a id="2597" href="Data.Graph.Acyclic.html#2569" class="Bound Operator">_∙_</a> <a id="2601" href="Data.Graph.Acyclic.html#2573" class="Bound">x</a> <a id="2603" href="Data.Graph.Acyclic.html#2580" class="Bound">g</a>

<a id="2606" class="Comment">-- &quot;Fold left&quot;.</a>

<a id="foldl" href="Data.Graph.Acyclic.html#foldl" class="Function">foldl</a> <a id="2629" class="Symbol">:</a> <a id="2631" class="Symbol">∀</a> <a id="2633" class="Symbol">{</a><a id="2634" href="Data.Graph.Acyclic.html#2634" class="Bound">N</a> <a id="2636" href="Data.Graph.Acyclic.html#2636" class="Bound">E</a> <a id="2638" href="Data.Graph.Acyclic.html#2638" class="Bound">n</a><a id="2639" class="Symbol">}</a> <a id="2641" class="Symbol">(</a><a id="2642" href="Data.Graph.Acyclic.html#2642" class="Bound">T</a> <a id="2644" class="Symbol">:</a> <a id="2646" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="2648" class="Symbol">→</a> <a id="2650" class="PrimitiveType">Set</a><a id="2653" class="Symbol">)</a> <a id="2655" class="Symbol">→</a>
        <a id="2665" class="Symbol">((</a><a id="2667" href="Data.Graph.Acyclic.html#2667" class="Bound">i</a> <a id="2669" class="Symbol">:</a> <a id="2671" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="2675" href="Data.Graph.Acyclic.html#2638" class="Bound">n</a><a id="2676" class="Symbol">)</a> <a id="2678" class="Symbol">→</a> <a id="2680" href="Data.Graph.Acyclic.html#2642" class="Bound">T</a> <a id="2682" class="Symbol">(</a><a id="2683" href="Data.Fin.html#to%E2%84%95" class="Function">toℕ</a> <a id="2687" href="Data.Graph.Acyclic.html#2667" class="Bound">i</a><a id="2688" class="Symbol">)</a> <a id="2690" class="Symbol">→</a> <a id="2692" href="Data.Graph.Acyclic.html#Context" class="Record">Context</a> <a id="2700" href="Data.Graph.Acyclic.html#2634" class="Bound">N</a> <a id="2702" href="Data.Graph.Acyclic.html#2636" class="Bound">E</a> <a id="2704" class="Symbol">(</a><a id="2705" href="Data.Graph.Acyclic.html#2638" class="Bound">n</a> <a id="2707" href="Data.Fin.html#_-_" class="Function Operator">-</a> <a id="2709" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="2713" href="Data.Graph.Acyclic.html#2667" class="Bound">i</a><a id="2714" class="Symbol">)</a> <a id="2716" class="Symbol">→</a>
         <a id="2727" href="Data.Graph.Acyclic.html#2642" class="Bound">T</a> <a id="2729" class="Symbol">(</a><a id="2730" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="2734" class="Symbol">(</a><a id="2735" href="Data.Fin.html#to%E2%84%95" class="Function">toℕ</a> <a id="2739" href="Data.Graph.Acyclic.html#2667" class="Bound">i</a><a id="2740" class="Symbol">)))</a> <a id="2744" class="Symbol">→</a>
        <a id="2754" href="Data.Graph.Acyclic.html#2642" class="Bound">T</a> <a id="2756" class="Number">0</a> <a id="2758" class="Symbol">→</a>
        <a id="2768" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="2774" href="Data.Graph.Acyclic.html#2634" class="Bound">N</a> <a id="2776" href="Data.Graph.Acyclic.html#2636" class="Bound">E</a> <a id="2778" href="Data.Graph.Acyclic.html#2638" class="Bound">n</a> <a id="2780" class="Symbol">→</a> <a id="2782" href="Data.Graph.Acyclic.html#2642" class="Bound">T</a> <a id="2784" href="Data.Graph.Acyclic.html#2638" class="Bound">n</a>
<a id="2786" href="Data.Graph.Acyclic.html#foldl" class="Function">foldl</a> <a id="2792" href="Data.Graph.Acyclic.html#2792" class="Bound">T</a> <a id="2794" href="Data.Graph.Acyclic.html#2794" class="Bound">f</a> <a id="2796" href="Data.Graph.Acyclic.html#2796" class="Bound">x</a> <a id="2798" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>       <a id="2806" class="Symbol">=</a> <a id="2808" href="Data.Graph.Acyclic.html#2796" class="Bound">x</a>
<a id="2810" href="Data.Graph.Acyclic.html#foldl" class="Function">foldl</a> <a id="2816" href="Data.Graph.Acyclic.html#2816" class="Bound">T</a> <a id="2818" href="Data.Graph.Acyclic.html#2818" class="Bound">f</a> <a id="2820" href="Data.Graph.Acyclic.html#2820" class="Bound">x</a> <a id="2822" class="Symbol">(</a><a id="2823" href="Data.Graph.Acyclic.html#2823" class="Bound">c</a> <a id="2825" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="2827" href="Data.Graph.Acyclic.html#2827" class="Bound">g</a><a id="2828" class="Symbol">)</a> <a id="2830" class="Symbol">=</a>
  <a id="2834" href="Data.Graph.Acyclic.html#foldl" class="Function">foldl</a> <a id="2840" class="Symbol">(λ</a> <a id="2843" href="Data.Graph.Acyclic.html#2843" class="Bound">n</a> <a id="2845" class="Symbol">→</a> <a id="2847" href="Data.Graph.Acyclic.html#2816" class="Bound">T</a> <a id="2849" class="Symbol">(</a><a id="2850" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="2854" href="Data.Graph.Acyclic.html#2843" class="Bound">n</a><a id="2855" class="Symbol">))</a> <a id="2858" class="Symbol">(λ</a> <a id="2861" href="Data.Graph.Acyclic.html#2861" class="Bound">i</a> <a id="2863" class="Symbol">→</a> <a id="2865" href="Data.Graph.Acyclic.html#2818" class="Bound">f</a> <a id="2867" class="Symbol">(</a><a id="2868" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="2872" href="Data.Graph.Acyclic.html#2861" class="Bound">i</a><a id="2873" class="Symbol">))</a> <a id="2876" class="Symbol">(</a><a id="2877" href="Data.Graph.Acyclic.html#2818" class="Bound">f</a> <a id="2879" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a> <a id="2884" href="Data.Graph.Acyclic.html#2820" class="Bound">x</a> <a id="2886" href="Data.Graph.Acyclic.html#2823" class="Bound">c</a><a id="2887" class="Symbol">)</a> <a id="2889" href="Data.Graph.Acyclic.html#2827" class="Bound">g</a>

<a id="2892" class="Comment">-- Maps over node contexts.</a>

<a id="map" href="Data.Graph.Acyclic.html#map" class="Function">map</a> <a id="2925" class="Symbol">:</a> <a id="2927" class="Symbol">∀</a> <a id="2929" class="Symbol">{</a><a id="2930" href="Data.Graph.Acyclic.html#2930" class="Bound">N₁</a> <a id="2933" href="Data.Graph.Acyclic.html#2933" class="Bound">N₂</a> <a id="2936" href="Data.Graph.Acyclic.html#2936" class="Bound">E₁</a> <a id="2939" href="Data.Graph.Acyclic.html#2939" class="Bound">E₂</a> <a id="2942" href="Data.Graph.Acyclic.html#2942" class="Bound">n</a><a id="2943" class="Symbol">}</a> <a id="2945" class="Symbol">→</a>
      <a id="2953" class="Symbol">(∀</a> <a id="2956" class="Symbol">{</a><a id="2957" href="Data.Graph.Acyclic.html#2957" class="Bound">n</a><a id="2958" class="Symbol">}</a> <a id="2960" class="Symbol">→</a> <a id="2962" href="Data.Graph.Acyclic.html#Context" class="Record">Context</a> <a id="2970" href="Data.Graph.Acyclic.html#2930" class="Bound">N₁</a> <a id="2973" href="Data.Graph.Acyclic.html#2936" class="Bound">E₁</a> <a id="2976" href="Data.Graph.Acyclic.html#2957" class="Bound">n</a> <a id="2978" class="Symbol">→</a> <a id="2980" href="Data.Graph.Acyclic.html#Context" class="Record">Context</a> <a id="2988" href="Data.Graph.Acyclic.html#2933" class="Bound">N₂</a> <a id="2991" href="Data.Graph.Acyclic.html#2939" class="Bound">E₂</a> <a id="2994" href="Data.Graph.Acyclic.html#2957" class="Bound">n</a><a id="2995" class="Symbol">)</a> <a id="2997" class="Symbol">→</a>
      <a id="3005" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="3011" href="Data.Graph.Acyclic.html#2930" class="Bound">N₁</a> <a id="3014" href="Data.Graph.Acyclic.html#2936" class="Bound">E₁</a> <a id="3017" href="Data.Graph.Acyclic.html#2942" class="Bound">n</a> <a id="3019" class="Symbol">→</a> <a id="3021" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="3027" href="Data.Graph.Acyclic.html#2933" class="Bound">N₂</a> <a id="3030" href="Data.Graph.Acyclic.html#2939" class="Bound">E₂</a> <a id="3033" href="Data.Graph.Acyclic.html#2942" class="Bound">n</a>
<a id="3035" href="Data.Graph.Acyclic.html#map" class="Function">map</a> <a id="3039" href="Data.Graph.Acyclic.html#3039" class="Bound">f</a> <a id="3041" class="Symbol">=</a> <a id="3043" href="Data.Graph.Acyclic.html#foldr" class="Function">foldr</a> <a id="3049" class="Symbol">_</a> <a id="3051" class="Symbol">(λ</a> <a id="3054" href="Data.Graph.Acyclic.html#3054" class="Bound">c</a> <a id="3056" href="Data.Graph.Acyclic.html#3056" class="Bound">g</a> <a id="3058" class="Symbol">→</a> <a id="3060" href="Data.Graph.Acyclic.html#3039" class="Bound">f</a> <a id="3062" href="Data.Graph.Acyclic.html#3054" class="Bound">c</a> <a id="3064" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="3066" href="Data.Graph.Acyclic.html#3056" class="Bound">g</a><a id="3067" class="Symbol">)</a> <a id="3069" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>

<a id="3072" class="Comment">-- Maps over node labels.</a>

<a id="nmap" href="Data.Graph.Acyclic.html#nmap" class="Function">nmap</a> <a id="3104" class="Symbol">:</a> <a id="3106" class="Symbol">∀</a> <a id="3108" class="Symbol">{</a><a id="3109" href="Data.Graph.Acyclic.html#3109" class="Bound">N₁</a> <a id="3112" href="Data.Graph.Acyclic.html#3112" class="Bound">N₂</a> <a id="3115" href="Data.Graph.Acyclic.html#3115" class="Bound">E</a> <a id="3117" href="Data.Graph.Acyclic.html#3117" class="Bound">n</a><a id="3118" class="Symbol">}</a> <a id="3120" class="Symbol">→</a> <a id="3122" class="Symbol">(</a><a id="3123" href="Data.Graph.Acyclic.html#3109" class="Bound">N₁</a> <a id="3126" class="Symbol">→</a> <a id="3128" href="Data.Graph.Acyclic.html#3112" class="Bound">N₂</a><a id="3130" class="Symbol">)</a> <a id="3132" class="Symbol">→</a> <a id="3134" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="3140" href="Data.Graph.Acyclic.html#3109" class="Bound">N₁</a> <a id="3143" href="Data.Graph.Acyclic.html#3115" class="Bound">E</a> <a id="3145" href="Data.Graph.Acyclic.html#3117" class="Bound">n</a> <a id="3147" class="Symbol">→</a> <a id="3149" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="3155" href="Data.Graph.Acyclic.html#3112" class="Bound">N₂</a> <a id="3158" href="Data.Graph.Acyclic.html#3115" class="Bound">E</a> <a id="3160" href="Data.Graph.Acyclic.html#3117" class="Bound">n</a>
<a id="3162" href="Data.Graph.Acyclic.html#nmap" class="Function">nmap</a> <a id="3167" href="Data.Graph.Acyclic.html#3167" class="Bound">f</a> <a id="3169" class="Symbol">=</a> <a id="3171" href="Data.Graph.Acyclic.html#map" class="Function">map</a> <a id="3175" class="Symbol">(</a><a id="3176" href="Data.Graph.Acyclic.html#cmap" class="Function">cmap</a> <a id="3181" href="Data.Graph.Acyclic.html#3167" class="Bound">f</a> <a id="3183" href="Function.html#id" class="Function">id</a><a id="3185" class="Symbol">)</a>

<a id="3188" class="Comment">-- Maps over edge labels.</a>

<a id="emap" href="Data.Graph.Acyclic.html#emap" class="Function">emap</a> <a id="3220" class="Symbol">:</a> <a id="3222" class="Symbol">∀</a> <a id="3224" class="Symbol">{</a><a id="3225" href="Data.Graph.Acyclic.html#3225" class="Bound">N</a> <a id="3227" href="Data.Graph.Acyclic.html#3227" class="Bound">E₁</a> <a id="3230" href="Data.Graph.Acyclic.html#3230" class="Bound">E₂</a> <a id="3233" href="Data.Graph.Acyclic.html#3233" class="Bound">n</a><a id="3234" class="Symbol">}</a> <a id="3236" class="Symbol">→</a> <a id="3238" class="Symbol">(</a><a id="3239" href="Data.Graph.Acyclic.html#3227" class="Bound">E₁</a> <a id="3242" class="Symbol">→</a> <a id="3244" href="Data.Graph.Acyclic.html#3230" class="Bound">E₂</a><a id="3246" class="Symbol">)</a> <a id="3248" class="Symbol">→</a> <a id="3250" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="3256" href="Data.Graph.Acyclic.html#3225" class="Bound">N</a> <a id="3258" href="Data.Graph.Acyclic.html#3227" class="Bound">E₁</a> <a id="3261" href="Data.Graph.Acyclic.html#3233" class="Bound">n</a> <a id="3263" class="Symbol">→</a> <a id="3265" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="3271" href="Data.Graph.Acyclic.html#3225" class="Bound">N</a> <a id="3273" href="Data.Graph.Acyclic.html#3230" class="Bound">E₂</a> <a id="3276" href="Data.Graph.Acyclic.html#3233" class="Bound">n</a>
<a id="3278" href="Data.Graph.Acyclic.html#emap" class="Function">emap</a> <a id="3283" href="Data.Graph.Acyclic.html#3283" class="Bound">f</a> <a id="3285" class="Symbol">=</a> <a id="3287" href="Data.Graph.Acyclic.html#map" class="Function">map</a> <a id="3291" class="Symbol">(</a><a id="3292" href="Data.Graph.Acyclic.html#cmap" class="Function">cmap</a> <a id="3297" href="Function.html#id" class="Function">id</a> <a id="3300" class="Symbol">(</a><a id="3301" href="Data.List.Base.html#map" class="Function">List.map</a> <a id="3310" class="Symbol">(</a><a id="3311" href="Data.Product.html#map" class="Function">Prod.map</a> <a id="3320" href="Data.Graph.Acyclic.html#3283" class="Bound">f</a> <a id="3322" href="Function.html#id" class="Function">id</a><a id="3324" class="Symbol">)))</a>

<a id="3329" class="Comment">-- Zips two graphs with the same number of nodes. Note that one of the</a>
<a id="3400" class="Comment">-- graphs has a type which restricts it to be completely disconnected.</a>

<a id="zipWith" href="Data.Graph.Acyclic.html#zipWith" class="Function">zipWith</a> <a id="3480" class="Symbol">:</a> <a id="3482" class="Symbol">∀</a> <a id="3484" class="Symbol">{</a><a id="3485" href="Data.Graph.Acyclic.html#3485" class="Bound">N₁</a> <a id="3488" href="Data.Graph.Acyclic.html#3488" class="Bound">N₂</a> <a id="3491" href="Data.Graph.Acyclic.html#3491" class="Bound">N</a> <a id="3493" href="Data.Graph.Acyclic.html#3493" class="Bound">E</a> <a id="3495" href="Data.Graph.Acyclic.html#3495" class="Bound">n</a><a id="3496" class="Symbol">}</a> <a id="3498" class="Symbol">→</a> <a id="3500" class="Symbol">(</a><a id="3501" href="Data.Graph.Acyclic.html#3485" class="Bound">N₁</a> <a id="3504" class="Symbol">→</a> <a id="3506" href="Data.Graph.Acyclic.html#3488" class="Bound">N₂</a> <a id="3509" class="Symbol">→</a> <a id="3511" href="Data.Graph.Acyclic.html#3491" class="Bound">N</a><a id="3512" class="Symbol">)</a> <a id="3514" class="Symbol">→</a>
          <a id="3526" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="3532" href="Data.Graph.Acyclic.html#3485" class="Bound">N₁</a> <a id="3535" href="Data.Empty.html#%E2%8A%A5" class="Datatype">⊥</a> <a id="3537" href="Data.Graph.Acyclic.html#3495" class="Bound">n</a> <a id="3539" class="Symbol">→</a> <a id="3541" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="3547" href="Data.Graph.Acyclic.html#3488" class="Bound">N₂</a> <a id="3550" href="Data.Graph.Acyclic.html#3493" class="Bound">E</a> <a id="3552" href="Data.Graph.Acyclic.html#3495" class="Bound">n</a> <a id="3554" class="Symbol">→</a> <a id="3556" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="3562" href="Data.Graph.Acyclic.html#3491" class="Bound">N</a> <a id="3564" href="Data.Graph.Acyclic.html#3493" class="Bound">E</a> <a id="3566" href="Data.Graph.Acyclic.html#3495" class="Bound">n</a>
<a id="3568" href="Data.Graph.Acyclic.html#zipWith" class="Function">zipWith</a> <a id="3576" href="Data.Graph.Acyclic.html#3576" class="Bound Operator">_∙_</a> <a id="3580" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>         <a id="3590" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>         <a id="3600" class="Symbol">=</a> <a id="3602" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>
<a id="3604" href="Data.Graph.Acyclic.html#zipWith" class="Function">zipWith</a> <a id="3612" href="Data.Graph.Acyclic.html#3612" class="Bound Operator">_∙_</a> <a id="3616" class="Symbol">(</a><a id="3617" href="Data.Graph.Acyclic.html#3617" class="Bound">c₁</a> <a id="3620" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="3622" href="Data.Graph.Acyclic.html#3622" class="Bound">g₁</a><a id="3624" class="Symbol">)</a> <a id="3626" class="Symbol">(</a><a id="3627" href="Data.Graph.Acyclic.html#3627" class="Bound">c₂</a> <a id="3630" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="3632" href="Data.Graph.Acyclic.html#3632" class="Bound">g₂</a><a id="3634" class="Symbol">)</a> <a id="3636" class="Symbol">=</a>
  <a id="3640" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="3648" class="Symbol">(</a><a id="3649" href="Data.Graph.Acyclic.html#Context.label" class="Field">label</a> <a id="3655" href="Data.Graph.Acyclic.html#3617" class="Bound">c₁</a> <a id="3658" href="Data.Graph.Acyclic.html#3612" class="Bound Operator">∙</a> <a id="3660" href="Data.Graph.Acyclic.html#Context.label" class="Field">label</a> <a id="3666" href="Data.Graph.Acyclic.html#3627" class="Bound">c₂</a><a id="3668" class="Symbol">)</a> <a id="3670" class="Symbol">(</a><a id="3671" href="Data.Graph.Acyclic.html#Context.successors" class="Field">successors</a> <a id="3682" href="Data.Graph.Acyclic.html#3627" class="Bound">c₂</a><a id="3684" class="Symbol">)</a> <a id="3686" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="3688" href="Data.Graph.Acyclic.html#zipWith" class="Function">zipWith</a> <a id="3696" href="Data.Graph.Acyclic.html#3612" class="Bound Operator">_∙_</a> <a id="3700" href="Data.Graph.Acyclic.html#3622" class="Bound">g₁</a> <a id="3703" href="Data.Graph.Acyclic.html#3632" class="Bound">g₂</a>

<a id="3707" class="Comment">------------------------------------------------------------------------</a>
<a id="3780" class="Comment">-- Specific graphs</a>

<a id="3800" class="Comment">-- A completeley disconnected graph.</a>

<a id="disconnected" href="Data.Graph.Acyclic.html#disconnected" class="Function">disconnected</a> <a id="3851" class="Symbol">:</a> <a id="3853" class="Symbol">∀</a> <a id="3855" href="Data.Graph.Acyclic.html#3855" class="Bound">n</a> <a id="3857" class="Symbol">→</a> <a id="3859" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="3865" href="Agda.Builtin.Unit.html#%E2%8A%A4" class="Record">⊤</a> <a id="3867" href="Data.Empty.html#%E2%8A%A5" class="Datatype">⊥</a> <a id="3869" href="Data.Graph.Acyclic.html#3855" class="Bound">n</a>
<a id="3871" href="Data.Graph.Acyclic.html#disconnected" class="Function">disconnected</a> <a id="3884" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a>    <a id="3892" class="Symbol">=</a> <a id="3894" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>
<a id="3896" href="Data.Graph.Acyclic.html#disconnected" class="Function">disconnected</a> <a id="3909" class="Symbol">(</a><a id="3910" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="3914" href="Data.Graph.Acyclic.html#3914" class="Bound">n</a><a id="3915" class="Symbol">)</a> <a id="3917" class="Symbol">=</a> <a id="3919" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="3927" href="Agda.Builtin.Unit.html#%E2%8A%A4.tt" class="InductiveConstructor">tt</a> <a id="3930" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a> <a id="3933" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="3935" href="Data.Graph.Acyclic.html#disconnected" class="Function">disconnected</a> <a id="3948" href="Data.Graph.Acyclic.html#3914" class="Bound">n</a>

<a id="3951" class="Comment">-- A complete graph.</a>

<a id="complete" href="Data.Graph.Acyclic.html#complete" class="Function">complete</a> <a id="3982" class="Symbol">:</a> <a id="3984" class="Symbol">∀</a> <a id="3986" href="Data.Graph.Acyclic.html#3986" class="Bound">n</a> <a id="3988" class="Symbol">→</a> <a id="3990" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="3996" href="Agda.Builtin.Unit.html#%E2%8A%A4" class="Record">⊤</a> <a id="3998" href="Agda.Builtin.Unit.html#%E2%8A%A4" class="Record">⊤</a> <a id="4000" href="Data.Graph.Acyclic.html#3986" class="Bound">n</a>
<a id="4002" href="Data.Graph.Acyclic.html#complete" class="Function">complete</a> <a id="4011" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a>    <a id="4019" class="Symbol">=</a> <a id="4021" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>
<a id="4023" href="Data.Graph.Acyclic.html#complete" class="Function">complete</a> <a id="4032" class="Symbol">(</a><a id="4033" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="4037" href="Data.Graph.Acyclic.html#4037" class="Bound">n</a><a id="4038" class="Symbol">)</a> <a id="4040" class="Symbol">=</a>
  <a id="4044" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="4052" href="Agda.Builtin.Unit.html#%E2%8A%A4.tt" class="InductiveConstructor">tt</a> <a id="4055" class="Symbol">(</a><a id="4056" href="Data.List.Base.html#map" class="Function">List.map</a> <a id="4065" class="Symbol">(</a><a id="4066" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">_,_</a> <a id="4070" href="Agda.Builtin.Unit.html#%E2%8A%A4.tt" class="InductiveConstructor">tt</a><a id="4072" class="Symbol">)</a> <a id="4074" href="Function.html#_%24_" class="Function Operator">$</a> <a id="4076" href="Data.Vec.html#toList" class="Function">Vec.toList</a> <a id="4087" class="Symbol">(</a><a id="4088" href="Data.Vec.html#allFin" class="Function">Vec.allFin</a> <a id="4099" href="Data.Graph.Acyclic.html#4037" class="Bound">n</a><a id="4100" class="Symbol">))</a> <a id="4103" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a>
  <a id="4107" href="Data.Graph.Acyclic.html#complete" class="Function">complete</a> <a id="4116" href="Data.Graph.Acyclic.html#4037" class="Bound">n</a>

<a id="4119" class="Comment">------------------------------------------------------------------------</a>
<a id="4192" class="Comment">-- Queries</a>

<a id="4204" class="Comment">-- The top-most context.</a>

<a id="head" href="Data.Graph.Acyclic.html#head" class="Function">head</a> <a id="4235" class="Symbol">:</a> <a id="4237" class="Symbol">∀</a> <a id="4239" class="Symbol">{</a><a id="4240" href="Data.Graph.Acyclic.html#4240" class="Bound">N</a> <a id="4242" href="Data.Graph.Acyclic.html#4242" class="Bound">E</a> <a id="4244" href="Data.Graph.Acyclic.html#4244" class="Bound">n</a><a id="4245" class="Symbol">}</a> <a id="4247" class="Symbol">→</a> <a id="4249" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="4255" href="Data.Graph.Acyclic.html#4240" class="Bound">N</a> <a id="4257" href="Data.Graph.Acyclic.html#4242" class="Bound">E</a> <a id="4259" class="Symbol">(</a><a id="4260" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="4264" href="Data.Graph.Acyclic.html#4244" class="Bound">n</a><a id="4265" class="Symbol">)</a> <a id="4267" class="Symbol">→</a> <a id="4269" href="Data.Graph.Acyclic.html#Context" class="Record">Context</a> <a id="4277" href="Data.Graph.Acyclic.html#4240" class="Bound">N</a> <a id="4279" href="Data.Graph.Acyclic.html#4242" class="Bound">E</a> <a id="4281" href="Data.Graph.Acyclic.html#4244" class="Bound">n</a>
<a id="4283" href="Data.Graph.Acyclic.html#head" class="Function">head</a> <a id="4288" class="Symbol">(</a><a id="4289" href="Data.Graph.Acyclic.html#4289" class="Bound">c</a> <a id="4291" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="4293" href="Data.Graph.Acyclic.html#4293" class="Bound">g</a><a id="4294" class="Symbol">)</a> <a id="4296" class="Symbol">=</a> <a id="4298" href="Data.Graph.Acyclic.html#4289" class="Bound">c</a>

<a id="4301" class="Comment">-- The remaining graph.</a>

<a id="tail" href="Data.Graph.Acyclic.html#tail" class="Function">tail</a> <a id="4331" class="Symbol">:</a> <a id="4333" class="Symbol">∀</a> <a id="4335" class="Symbol">{</a><a id="4336" href="Data.Graph.Acyclic.html#4336" class="Bound">N</a> <a id="4338" href="Data.Graph.Acyclic.html#4338" class="Bound">E</a> <a id="4340" href="Data.Graph.Acyclic.html#4340" class="Bound">n</a><a id="4341" class="Symbol">}</a> <a id="4343" class="Symbol">→</a> <a id="4345" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="4351" href="Data.Graph.Acyclic.html#4336" class="Bound">N</a> <a id="4353" href="Data.Graph.Acyclic.html#4338" class="Bound">E</a> <a id="4355" class="Symbol">(</a><a id="4356" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="4360" href="Data.Graph.Acyclic.html#4340" class="Bound">n</a><a id="4361" class="Symbol">)</a> <a id="4363" class="Symbol">→</a> <a id="4365" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="4371" href="Data.Graph.Acyclic.html#4336" class="Bound">N</a> <a id="4373" href="Data.Graph.Acyclic.html#4338" class="Bound">E</a> <a id="4375" href="Data.Graph.Acyclic.html#4340" class="Bound">n</a>
<a id="4377" href="Data.Graph.Acyclic.html#tail" class="Function">tail</a> <a id="4382" class="Symbol">(</a><a id="4383" href="Data.Graph.Acyclic.html#4383" class="Bound">c</a> <a id="4385" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="4387" href="Data.Graph.Acyclic.html#4387" class="Bound">g</a><a id="4388" class="Symbol">)</a> <a id="4390" class="Symbol">=</a> <a id="4392" href="Data.Graph.Acyclic.html#4387" class="Bound">g</a>

<a id="4395" class="Comment">-- Finds the context and remaining graph corresponding to a given node</a>
<a id="4466" class="Comment">-- index.</a>

<a id="_[_]" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">_[_]</a> <a id="4482" class="Symbol">:</a> <a id="4484" class="Symbol">∀</a> <a id="4486" class="Symbol">{</a><a id="4487" href="Data.Graph.Acyclic.html#4487" class="Bound">N</a> <a id="4489" href="Data.Graph.Acyclic.html#4489" class="Bound">E</a> <a id="4491" href="Data.Graph.Acyclic.html#4491" class="Bound">n</a><a id="4492" class="Symbol">}</a> <a id="4494" class="Symbol">→</a>
       <a id="4503" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="4509" href="Data.Graph.Acyclic.html#4487" class="Bound">N</a> <a id="4511" href="Data.Graph.Acyclic.html#4489" class="Bound">E</a> <a id="4513" href="Data.Graph.Acyclic.html#4491" class="Bound">n</a> <a id="4515" class="Symbol">→</a> <a id="4517" class="Symbol">(</a><a id="4518" href="Data.Graph.Acyclic.html#4518" class="Bound">i</a> <a id="4520" class="Symbol">:</a> <a id="4522" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="4526" href="Data.Graph.Acyclic.html#4491" class="Bound">n</a><a id="4527" class="Symbol">)</a> <a id="4529" class="Symbol">→</a> <a id="4531" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="4537" href="Data.Graph.Acyclic.html#4487" class="Bound">N</a> <a id="4539" href="Data.Graph.Acyclic.html#4489" class="Bound">E</a> <a id="4541" class="Symbol">(</a><a id="4542" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="4546" class="Symbol">(</a><a id="4547" href="Data.Graph.Acyclic.html#4491" class="Bound">n</a> <a id="4549" href="Data.Fin.html#_-_" class="Function Operator">-</a> <a id="4551" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="4555" href="Data.Graph.Acyclic.html#4518" class="Bound">i</a><a id="4556" class="Symbol">))</a>
<a id="4559" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>       <a id="4567" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">[</a> <a id="4569" class="Symbol">()</a> <a id="4572" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">]</a>
<a id="4574" class="Symbol">(</a><a id="4575" href="Data.Graph.Acyclic.html#4575" class="Bound">c</a> <a id="4577" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="4579" href="Data.Graph.Acyclic.html#4579" class="Bound">g</a><a id="4580" class="Symbol">)</a> <a id="4582" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">[</a> <a id="4584" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a> <a id="4589" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">]</a>  <a id="4592" class="Symbol">=</a> <a id="4594" href="Data.Graph.Acyclic.html#4575" class="Bound">c</a> <a id="4596" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="4598" href="Data.Graph.Acyclic.html#4579" class="Bound">g</a>
<a id="4600" class="Symbol">(</a><a id="4601" href="Data.Graph.Acyclic.html#4601" class="Bound">c</a> <a id="4603" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="4605" href="Data.Graph.Acyclic.html#4605" class="Bound">g</a><a id="4606" class="Symbol">)</a> <a id="4608" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">[</a> <a id="4610" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="4614" href="Data.Graph.Acyclic.html#4614" class="Bound">i</a> <a id="4616" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">]</a> <a id="4618" class="Symbol">=</a> <a id="4620" href="Data.Graph.Acyclic.html#4605" class="Bound">g</a> <a id="4622" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">[</a> <a id="4624" href="Data.Graph.Acyclic.html#4614" class="Bound">i</a> <a id="4626" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">]</a>

<a id="4629" class="Comment">-- The nodes of the graph (node number relative to &quot;topmost&quot; node ×</a>
<a id="4697" class="Comment">-- node label).</a>

<a id="nodes" href="Data.Graph.Acyclic.html#nodes" class="Function">nodes</a> <a id="4720" class="Symbol">:</a> <a id="4722" class="Symbol">∀</a> <a id="4724" class="Symbol">{</a><a id="4725" href="Data.Graph.Acyclic.html#4725" class="Bound">N</a> <a id="4727" href="Data.Graph.Acyclic.html#4727" class="Bound">E</a> <a id="4729" href="Data.Graph.Acyclic.html#4729" class="Bound">n</a><a id="4730" class="Symbol">}</a> <a id="4732" class="Symbol">→</a> <a id="4734" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="4740" href="Data.Graph.Acyclic.html#4725" class="Bound">N</a> <a id="4742" href="Data.Graph.Acyclic.html#4727" class="Bound">E</a> <a id="4744" href="Data.Graph.Acyclic.html#4729" class="Bound">n</a> <a id="4746" class="Symbol">→</a> <a id="4748" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="4752" class="Symbol">(</a><a id="4753" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="4757" href="Data.Graph.Acyclic.html#4729" class="Bound">n</a> <a id="4759" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="4761" href="Data.Graph.Acyclic.html#4725" class="Bound">N</a><a id="4762" class="Symbol">)</a> <a id="4764" href="Data.Graph.Acyclic.html#4729" class="Bound">n</a>
<a id="4766" href="Data.Graph.Acyclic.html#nodes" class="Function">nodes</a> <a id="4772" class="Symbol">{</a><a id="4773" href="Data.Graph.Acyclic.html#4773" class="Bound">N</a><a id="4774" class="Symbol">}</a> <a id="4776" class="Symbol">=</a> <a id="4778" href="Data.Vec.html#zip" class="Function">Vec.zip</a> <a id="4786" class="Symbol">(</a><a id="4787" href="Data.Vec.html#allFin" class="Function">Vec.allFin</a> <a id="4798" class="Symbol">_)</a> <a id="4801" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a>
            <a id="4815" href="Data.Graph.Acyclic.html#foldr" class="Function">foldr</a> <a id="4821" class="Symbol">(</a><a id="4822" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="4826" href="Data.Graph.Acyclic.html#4773" class="Bound">N</a><a id="4827" class="Symbol">)</a> <a id="4829" class="Symbol">(λ</a> <a id="4832" href="Data.Graph.Acyclic.html#4832" class="Bound">c</a> <a id="4834" href="Data.Graph.Acyclic.html#4834" class="Bound">ns</a> <a id="4837" class="Symbol">→</a> <a id="4839" href="Data.Graph.Acyclic.html#Context.label" class="Field">label</a> <a id="4845" href="Data.Graph.Acyclic.html#4832" class="Bound">c</a> <a id="4847" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="4849" href="Data.Graph.Acyclic.html#4834" class="Bound">ns</a><a id="4851" class="Symbol">)</a> <a id="4853" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a>

<a id="4857" class="Keyword">private</a>

  <a id="test-nodes" href="Data.Graph.Acyclic.html#test-nodes" class="Function">test-nodes</a> <a id="4879" class="Symbol">:</a> <a id="4881" href="Data.Graph.Acyclic.html#nodes" class="Function">nodes</a> <a id="4887" href="Data.Graph.Acyclic.html#example" class="Function">example</a> <a id="4895" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="4897" class="Symbol">(</a><a id="4898" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="4900" class="Number">0</a> <a id="4902" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4904" class="Number">0</a><a id="4905" class="Symbol">)</a> <a id="4907" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="4909" class="Symbol">(</a><a id="4910" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="4912" class="Number">1</a> <a id="4914" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4916" class="Number">1</a><a id="4917" class="Symbol">)</a> <a id="4919" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="4921" class="Symbol">(</a><a id="4922" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="4924" class="Number">2</a> <a id="4926" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4928" class="Number">2</a><a id="4929" class="Symbol">)</a> <a id="4931" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a>
                               <a id="4964" class="Symbol">(</a><a id="4965" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="4967" class="Number">3</a> <a id="4969" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4971" class="Number">3</a><a id="4972" class="Symbol">)</a> <a id="4974" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="4976" class="Symbol">(</a><a id="4977" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="4979" class="Number">4</a> <a id="4981" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4983" class="Number">4</a><a id="4984" class="Symbol">)</a> <a id="4986" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="4988" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a>
  <a id="4993" href="Data.Graph.Acyclic.html#test-nodes" class="Function">test-nodes</a> <a id="5004" class="Symbol">=</a> <a id="5006" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a>

<a id="5014" class="Comment">-- Topological sort. Gives a vector where earlier nodes are never</a>
<a id="5080" class="Comment">-- successors of later nodes.</a>

<a id="topSort" href="Data.Graph.Acyclic.html#topSort" class="Function">topSort</a> <a id="5119" class="Symbol">:</a> <a id="5121" class="Symbol">∀</a> <a id="5123" class="Symbol">{</a><a id="5124" href="Data.Graph.Acyclic.html#5124" class="Bound">N</a> <a id="5126" href="Data.Graph.Acyclic.html#5126" class="Bound">E</a> <a id="5128" href="Data.Graph.Acyclic.html#5128" class="Bound">n</a><a id="5129" class="Symbol">}</a> <a id="5131" class="Symbol">→</a> <a id="5133" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="5139" href="Data.Graph.Acyclic.html#5124" class="Bound">N</a> <a id="5141" href="Data.Graph.Acyclic.html#5126" class="Bound">E</a> <a id="5143" href="Data.Graph.Acyclic.html#5128" class="Bound">n</a> <a id="5145" class="Symbol">→</a> <a id="5147" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="5151" class="Symbol">(</a><a id="5152" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="5156" href="Data.Graph.Acyclic.html#5128" class="Bound">n</a> <a id="5158" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="5160" href="Data.Graph.Acyclic.html#5124" class="Bound">N</a><a id="5161" class="Symbol">)</a> <a id="5163" href="Data.Graph.Acyclic.html#5128" class="Bound">n</a>
<a id="5165" href="Data.Graph.Acyclic.html#topSort" class="Function">topSort</a> <a id="5173" class="Symbol">=</a> <a id="5175" href="Data.Graph.Acyclic.html#nodes" class="Function">nodes</a>

<a id="5182" class="Comment">-- The edges of the graph (predecessor × edge label × successor).</a>
<a id="5248" class="Comment">--</a>
<a id="5251" class="Comment">-- The predecessor is a node number relative to the &quot;topmost&quot; node in</a>
<a id="5321" class="Comment">-- the graph, and the successor is a node number relative to the</a>
<a id="5386" class="Comment">-- predecessor.</a>

<a id="edges" href="Data.Graph.Acyclic.html#edges" class="Function">edges</a> <a id="5409" class="Symbol">:</a> <a id="5411" class="Symbol">∀</a> <a id="5413" class="Symbol">{</a><a id="5414" href="Data.Graph.Acyclic.html#5414" class="Bound">E</a> <a id="5416" href="Data.Graph.Acyclic.html#5416" class="Bound">N</a> <a id="5418" href="Data.Graph.Acyclic.html#5418" class="Bound">n</a><a id="5419" class="Symbol">}</a> <a id="5421" class="Symbol">→</a> <a id="5423" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="5429" href="Data.Graph.Acyclic.html#5416" class="Bound">N</a> <a id="5431" href="Data.Graph.Acyclic.html#5414" class="Bound">E</a> <a id="5433" href="Data.Graph.Acyclic.html#5418" class="Bound">n</a> <a id="5435" class="Symbol">→</a> <a id="5437" href="Agda.Builtin.List.html#List" class="Datatype">List</a> <a id="5442" class="Symbol">(</a><a id="5443" href="Data.Product.html#%E2%88%83" class="Function">∃</a> <a id="5445" class="Symbol">λ</a> <a id="5447" href="Data.Graph.Acyclic.html#5447" class="Bound">i</a> <a id="5449" class="Symbol">→</a> <a id="5451" href="Data.Graph.Acyclic.html#5414" class="Bound">E</a> <a id="5453" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="5455" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="5459" class="Symbol">(</a><a id="5460" href="Data.Graph.Acyclic.html#5418" class="Bound">n</a> <a id="5462" href="Data.Fin.html#_-_" class="Function Operator">-</a> <a id="5464" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="5468" href="Data.Graph.Acyclic.html#5447" class="Bound">i</a><a id="5469" class="Symbol">))</a>
<a id="5472" href="Data.Graph.Acyclic.html#edges" class="Function">edges</a> <a id="5478" class="Symbol">{</a><a id="5479" href="Data.Graph.Acyclic.html#5479" class="Bound">E</a><a id="5480" class="Symbol">}</a> <a id="5482" class="Symbol">{</a><a id="5483" href="Data.Graph.Acyclic.html#5483" class="Bound">N</a><a id="5484" class="Symbol">}</a> <a id="5486" class="Symbol">{</a><a id="5487" href="Data.Graph.Acyclic.html#5487" class="Bound">n</a><a id="5488" class="Symbol">}</a> <a id="5490" class="Symbol">=</a>
  <a id="5494" href="Data.Graph.Acyclic.html#foldl" class="Function">foldl</a> <a id="5500" class="Symbol">(λ</a> <a id="5503" href="Data.Graph.Acyclic.html#5503" class="Bound">_</a> <a id="5505" class="Symbol">→</a> <a id="5507" href="Agda.Builtin.List.html#List" class="Datatype">List</a> <a id="5512" class="Symbol">(</a><a id="5513" href="Data.Product.html#%E2%88%83" class="Function">∃</a> <a id="5515" class="Symbol">λ</a> <a id="5517" href="Data.Graph.Acyclic.html#5517" class="Bound">i</a> <a id="5519" class="Symbol">→</a> <a id="5521" href="Data.Graph.Acyclic.html#5479" class="Bound">E</a> <a id="5523" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="5525" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="5529" class="Symbol">(</a><a id="5530" href="Data.Graph.Acyclic.html#5487" class="Bound">n</a> <a id="5532" href="Data.Fin.html#_-_" class="Function Operator">-</a> <a id="5534" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="5538" href="Data.Graph.Acyclic.html#5517" class="Bound">i</a><a id="5539" class="Symbol">)))</a>
        <a id="5551" class="Symbol">(λ</a> <a id="5554" href="Data.Graph.Acyclic.html#5554" class="Bound">i</a> <a id="5556" href="Data.Graph.Acyclic.html#5556" class="Bound">es</a> <a id="5559" href="Data.Graph.Acyclic.html#5559" class="Bound">c</a> <a id="5561" class="Symbol">→</a> <a id="5563" href="Data.List.Base.html#_%2B%2B_" class="Function Operator">List._++_</a> <a id="5573" href="Data.Graph.Acyclic.html#5556" class="Bound">es</a> <a id="5576" class="Symbol">(</a><a id="5577" href="Data.List.Base.html#map" class="Function">List.map</a> <a id="5586" class="Symbol">(</a><a id="5587" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">_,_</a> <a id="5591" href="Data.Graph.Acyclic.html#5554" class="Bound">i</a><a id="5592" class="Symbol">)</a> <a id="5594" class="Symbol">(</a><a id="5595" href="Data.Graph.Acyclic.html#Context.successors" class="Field">successors</a> <a id="5606" href="Data.Graph.Acyclic.html#5559" class="Bound">c</a><a id="5607" class="Symbol">)))</a>
        <a id="5619" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a>

<a id="5623" class="Keyword">private</a>

  <a id="test-edges" href="Data.Graph.Acyclic.html#test-edges" class="Function">test-edges</a> <a id="5645" class="Symbol">:</a> <a id="5647" href="Data.Graph.Acyclic.html#edges" class="Function">edges</a> <a id="5653" href="Data.Graph.Acyclic.html#example" class="Function">example</a> <a id="5661" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="5663" class="Symbol">(</a><a id="5664" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="5666" class="Number">1</a> <a id="5668" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5670" class="Number">10</a> <a id="5673" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5675" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="5677" class="Number">1</a><a id="5678" class="Symbol">)</a> <a id="5680" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="5682" class="Symbol">(</a><a id="5683" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="5685" class="Number">1</a> <a id="5687" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5689" class="Number">11</a> <a id="5692" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5694" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="5696" class="Number">1</a><a id="5697" class="Symbol">)</a> <a id="5699" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a>
                               <a id="5732" class="Symbol">(</a><a id="5733" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="5735" class="Number">2</a> <a id="5737" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5739" class="Number">12</a> <a id="5742" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5744" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="5746" class="Number">0</a><a id="5747" class="Symbol">)</a> <a id="5749" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="5751" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a>
  <a id="5756" href="Data.Graph.Acyclic.html#test-edges" class="Function">test-edges</a> <a id="5767" class="Symbol">=</a> <a id="5769" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a>

<a id="5777" class="Comment">-- The successors of a given node i (edge label × node number relative</a>
<a id="5848" class="Comment">-- to i).</a>

<a id="sucs" href="Data.Graph.Acyclic.html#sucs" class="Function">sucs</a> <a id="5864" class="Symbol">:</a> <a id="5866" class="Symbol">∀</a> <a id="5868" class="Symbol">{</a><a id="5869" href="Data.Graph.Acyclic.html#5869" class="Bound">E</a> <a id="5871" href="Data.Graph.Acyclic.html#5871" class="Bound">N</a> <a id="5873" href="Data.Graph.Acyclic.html#5873" class="Bound">n</a><a id="5874" class="Symbol">}</a> <a id="5876" class="Symbol">→</a>
       <a id="5885" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="5891" href="Data.Graph.Acyclic.html#5871" class="Bound">N</a> <a id="5893" href="Data.Graph.Acyclic.html#5869" class="Bound">E</a> <a id="5895" href="Data.Graph.Acyclic.html#5873" class="Bound">n</a> <a id="5897" class="Symbol">→</a> <a id="5899" class="Symbol">(</a><a id="5900" href="Data.Graph.Acyclic.html#5900" class="Bound">i</a> <a id="5902" class="Symbol">:</a> <a id="5904" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="5908" href="Data.Graph.Acyclic.html#5873" class="Bound">n</a><a id="5909" class="Symbol">)</a> <a id="5911" class="Symbol">→</a> <a id="5913" href="Agda.Builtin.List.html#List" class="Datatype">List</a> <a id="5918" class="Symbol">(</a><a id="5919" href="Data.Graph.Acyclic.html#5869" class="Bound">E</a> <a id="5921" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="5923" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="5927" class="Symbol">(</a><a id="5928" href="Data.Graph.Acyclic.html#5873" class="Bound">n</a> <a id="5930" href="Data.Fin.html#_-_" class="Function Operator">-</a> <a id="5932" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="5936" href="Data.Graph.Acyclic.html#5900" class="Bound">i</a><a id="5937" class="Symbol">))</a>
<a id="5940" href="Data.Graph.Acyclic.html#sucs" class="Function">sucs</a> <a id="5945" href="Data.Graph.Acyclic.html#5945" class="Bound">g</a> <a id="5947" href="Data.Graph.Acyclic.html#5947" class="Bound">i</a> <a id="5949" class="Symbol">=</a> <a id="5951" href="Data.Graph.Acyclic.html#Context.successors" class="Field">successors</a> <a id="5962" href="Function.html#_%24_" class="Function Operator">$</a> <a id="5964" href="Data.Graph.Acyclic.html#head" class="Function">head</a> <a id="5969" class="Symbol">(</a><a id="5970" href="Data.Graph.Acyclic.html#5945" class="Bound">g</a> <a id="5972" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">[</a> <a id="5974" href="Data.Graph.Acyclic.html#5947" class="Bound">i</a> <a id="5976" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">]</a><a id="5977" class="Symbol">)</a>

<a id="5980" class="Keyword">private</a>

  <a id="test-sucs" href="Data.Graph.Acyclic.html#test-sucs" class="Function">test-sucs</a> <a id="6001" class="Symbol">:</a> <a id="6003" href="Data.Graph.Acyclic.html#sucs" class="Function">sucs</a> <a id="6008" href="Data.Graph.Acyclic.html#example" class="Function">example</a> <a id="6016" class="Symbol">(</a><a id="6017" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="6019" class="Number">1</a><a id="6020" class="Symbol">)</a> <a id="6022" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="6024" class="Symbol">(</a><a id="6025" class="Number">10</a> <a id="6028" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6030" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="6032" class="Number">1</a><a id="6033" class="Symbol">)</a> <a id="6035" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="6037" class="Symbol">(</a><a id="6038" class="Number">11</a> <a id="6041" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6043" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="6045" class="Number">1</a><a id="6046" class="Symbol">)</a> <a id="6048" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="6050" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a>
  <a id="6055" href="Data.Graph.Acyclic.html#test-sucs" class="Function">test-sucs</a> <a id="6065" class="Symbol">=</a> <a id="6067" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a>

<a id="6075" class="Comment">-- The predecessors of a given node i (node number relative to i ×</a>
<a id="6142" class="Comment">-- edge label).</a>

<a id="preds" href="Data.Graph.Acyclic.html#preds" class="Function">preds</a> <a id="6165" class="Symbol">:</a> <a id="6167" class="Symbol">∀</a> <a id="6169" class="Symbol">{</a><a id="6170" href="Data.Graph.Acyclic.html#6170" class="Bound">E</a> <a id="6172" href="Data.Graph.Acyclic.html#6172" class="Bound">N</a> <a id="6174" href="Data.Graph.Acyclic.html#6174" class="Bound">n</a><a id="6175" class="Symbol">}</a> <a id="6177" class="Symbol">→</a> <a id="6179" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="6185" href="Data.Graph.Acyclic.html#6172" class="Bound">N</a> <a id="6187" href="Data.Graph.Acyclic.html#6170" class="Bound">E</a> <a id="6189" href="Data.Graph.Acyclic.html#6174" class="Bound">n</a> <a id="6191" class="Symbol">→</a> <a id="6193" class="Symbol">(</a><a id="6194" href="Data.Graph.Acyclic.html#6194" class="Bound">i</a> <a id="6196" class="Symbol">:</a> <a id="6198" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="6202" href="Data.Graph.Acyclic.html#6174" class="Bound">n</a><a id="6203" class="Symbol">)</a> <a id="6205" class="Symbol">→</a> <a id="6207" href="Agda.Builtin.List.html#List" class="Datatype">List</a> <a id="6212" class="Symbol">(</a><a id="6213" href="Data.Fin.html#Fin%E2%80%B2" class="Function">Fin′</a> <a id="6218" href="Data.Graph.Acyclic.html#6194" class="Bound">i</a> <a id="6220" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="6222" href="Data.Graph.Acyclic.html#6170" class="Bound">E</a><a id="6223" class="Symbol">)</a>
<a id="6225" href="Data.Graph.Acyclic.html#preds" class="Function">preds</a> <a id="6231" href="Data.Graph.Acyclic.html#6231" class="Bound">g</a>       <a id="6239" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a>    <a id="6247" class="Symbol">=</a> <a id="6249" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a>
<a id="6252" href="Data.Graph.Acyclic.html#preds" class="Function">preds</a> <a id="6258" class="Symbol">(</a><a id="6259" href="Data.Graph.Acyclic.html#6259" class="Bound">c</a> <a id="6261" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="6263" href="Data.Graph.Acyclic.html#6263" class="Bound">g</a><a id="6264" class="Symbol">)</a> <a id="6266" class="Symbol">(</a><a id="6267" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="6271" href="Data.Graph.Acyclic.html#6271" class="Bound">i</a><a id="6272" class="Symbol">)</a> <a id="6274" class="Symbol">=</a>
  <a id="6278" href="Data.List.Base.html#_%2B%2B_" class="Function Operator">List._++_</a> <a id="6288" class="Symbol">(</a><a id="6289" href="Data.List.Base.html#gfilter" class="Function">List.gfilter</a> <a id="6302" class="Symbol">(</a><a id="6303" href="Data.Graph.Acyclic.html#6387" class="Function">p</a> <a id="6305" href="Data.Graph.Acyclic.html#6271" class="Bound">i</a><a id="6306" class="Symbol">)</a> <a id="6308" href="Function.html#_%24_" class="Function Operator">$</a> <a id="6310" href="Data.Graph.Acyclic.html#Context.successors" class="Field">successors</a> <a id="6321" href="Data.Graph.Acyclic.html#6259" class="Bound">c</a><a id="6322" class="Symbol">)</a>
            <a id="6336" class="Symbol">(</a><a id="6337" href="Data.List.Base.html#map" class="Function">List.map</a> <a id="6346" class="Symbol">(</a><a id="6347" href="Data.Product.html#map" class="Function">Prod.map</a> <a id="6356" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="6360" href="Function.html#id" class="Function">id</a><a id="6362" class="Symbol">)</a> <a id="6364" href="Function.html#_%24_" class="Function Operator">$</a> <a id="6366" href="Data.Graph.Acyclic.html#preds" class="Function">preds</a> <a id="6372" href="Data.Graph.Acyclic.html#6263" class="Bound">g</a> <a id="6374" href="Data.Graph.Acyclic.html#6271" class="Bound">i</a><a id="6375" class="Symbol">)</a>
  <a id="6379" class="Keyword">where</a>
  <a id="6387" href="Data.Graph.Acyclic.html#6387" class="Function">p</a> <a id="6389" class="Symbol">:</a> <a id="6391" class="Symbol">∀</a> <a id="6393" class="Symbol">{</a><a id="6394" href="Data.Graph.Acyclic.html#6394" class="Bound">E</a> <a id="6396" class="Symbol">:</a> <a id="6398" class="PrimitiveType">Set</a><a id="6401" class="Symbol">}</a> <a id="6403" class="Symbol">{</a><a id="6404" href="Data.Graph.Acyclic.html#6404" class="Bound">n</a><a id="6405" class="Symbol">}</a> <a id="6407" class="Symbol">(</a><a id="6408" href="Data.Graph.Acyclic.html#6408" class="Bound">i</a> <a id="6410" class="Symbol">:</a> <a id="6412" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="6416" href="Data.Graph.Acyclic.html#6404" class="Bound">n</a><a id="6417" class="Symbol">)</a> <a id="6419" class="Symbol">→</a> <a id="6421" href="Data.Graph.Acyclic.html#6394" class="Bound">E</a> <a id="6423" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="6425" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="6429" href="Data.Graph.Acyclic.html#6404" class="Bound">n</a> <a id="6431" class="Symbol">→</a> <a id="6433" href="Data.Maybe.Base.html#Maybe" class="Datatype">Maybe</a> <a id="6439" class="Symbol">(</a><a id="6440" href="Data.Fin.html#Fin%E2%80%B2" class="Function">Fin′</a> <a id="6445" class="Symbol">(</a><a id="6446" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="6450" href="Data.Graph.Acyclic.html#6408" class="Bound">i</a><a id="6451" class="Symbol">)</a> <a id="6453" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="6455" href="Data.Graph.Acyclic.html#6394" class="Bound">E</a><a id="6456" class="Symbol">)</a>
  <a id="6460" href="Data.Graph.Acyclic.html#6387" class="Function">p</a> <a id="6462" href="Data.Graph.Acyclic.html#6462" class="Bound">i</a> <a id="6464" class="Symbol">(</a><a id="6465" href="Data.Graph.Acyclic.html#6465" class="Bound">e</a> <a id="6467" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6469" href="Data.Graph.Acyclic.html#6469" class="Bound">j</a><a id="6470" class="Symbol">)</a>  <a id="6473" class="Keyword">with</a> <a id="6478" href="Data.Graph.Acyclic.html#6462" class="Bound">i</a> <a id="6480" href="Data.Fin.Properties.html#_%E2%89%9F_" class="Function Operator">≟</a> <a id="6482" href="Data.Graph.Acyclic.html#6469" class="Bound">j</a>
  <a id="6486" href="Data.Graph.Acyclic.html#6387" class="Function">p</a> <a id="6488" href="Data.Graph.Acyclic.html#6488" class="Bound">i</a> <a id="6490" class="Symbol">(</a><a id="6491" href="Data.Graph.Acyclic.html#6491" class="Bound">e</a> <a id="6493" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6495" class="DottedPattern Symbol">.</a><a id="6496" href="Data.Graph.Acyclic.html#6488" class="DottedPattern Bound">i</a><a id="6497" class="Symbol">)</a> <a id="6499" class="Symbol">|</a> <a id="6501" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="6505" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a> <a id="6512" class="Symbol">=</a> <a id="6514" href="Data.Maybe.Base.html#Maybe.just" class="InductiveConstructor">just</a> <a id="6519" class="Symbol">(</a><a id="6520" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a> <a id="6525" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6527" href="Data.Graph.Acyclic.html#6491" class="Bound">e</a><a id="6528" class="Symbol">)</a>
  <a id="6532" href="Data.Graph.Acyclic.html#6387" class="Function">p</a> <a id="6534" href="Data.Graph.Acyclic.html#6534" class="Bound">i</a> <a id="6536" class="Symbol">(</a><a id="6537" href="Data.Graph.Acyclic.html#6537" class="Bound">e</a> <a id="6539" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6541" href="Data.Graph.Acyclic.html#6541" class="Bound">j</a><a id="6542" class="Symbol">)</a>  <a id="6545" class="Symbol">|</a> <a id="6547" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="6550" class="Symbol">_</a>       <a id="6558" class="Symbol">=</a> <a id="6560" href="Data.Maybe.Base.html#Maybe.nothing" class="InductiveConstructor">nothing</a>

<a id="6569" class="Keyword">private</a>

  <a id="test-preds" href="Data.Graph.Acyclic.html#test-preds" class="Function">test-preds</a> <a id="6591" class="Symbol">:</a> <a id="6593" href="Data.Graph.Acyclic.html#preds" class="Function">preds</a> <a id="6599" href="Data.Graph.Acyclic.html#example" class="Function">example</a> <a id="6607" class="Symbol">(</a><a id="6608" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="6610" class="Number">3</a><a id="6611" class="Symbol">)</a> <a id="6613" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a>
               <a id="6630" class="Symbol">(</a><a id="6631" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="6633" class="Number">1</a> <a id="6635" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6637" class="Number">10</a><a id="6639" class="Symbol">)</a> <a id="6641" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="6643" class="Symbol">(</a><a id="6644" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="6646" class="Number">1</a> <a id="6648" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6650" class="Number">11</a><a id="6652" class="Symbol">)</a> <a id="6654" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="6656" class="Symbol">(</a><a id="6657" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="6659" class="Number">2</a> <a id="6661" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6663" class="Number">12</a><a id="6665" class="Symbol">)</a> <a id="6667" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="6669" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a>
  <a id="6674" href="Data.Graph.Acyclic.html#test-preds" class="Function">test-preds</a> <a id="6685" class="Symbol">=</a> <a id="6687" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a>

<a id="6695" class="Comment">------------------------------------------------------------------------</a>
<a id="6768" class="Comment">-- Operations</a>

<a id="6783" class="Comment">-- Weakens a node label.</a>

<a id="weaken" href="Data.Graph.Acyclic.html#weaken" class="Function">weaken</a> <a id="6816" class="Symbol">:</a> <a id="6818" class="Symbol">∀</a> <a id="6820" class="Symbol">{</a><a id="6821" href="Data.Graph.Acyclic.html#6821" class="Bound">n</a><a id="6822" class="Symbol">}</a> <a id="6824" class="Symbol">{</a><a id="6825" href="Data.Graph.Acyclic.html#6825" class="Bound">i</a> <a id="6827" class="Symbol">:</a> <a id="6829" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="6833" href="Data.Graph.Acyclic.html#6821" class="Bound">n</a><a id="6834" class="Symbol">}</a> <a id="6836" class="Symbol">→</a> <a id="6838" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="6842" class="Symbol">(</a><a id="6843" href="Data.Graph.Acyclic.html#6821" class="Bound">n</a> <a id="6845" href="Data.Fin.html#_-_" class="Function Operator">-</a> <a id="6847" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="6851" href="Data.Graph.Acyclic.html#6825" class="Bound">i</a><a id="6852" class="Symbol">)</a> <a id="6854" class="Symbol">→</a> <a id="6856" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="6860" href="Data.Graph.Acyclic.html#6821" class="Bound">n</a>
<a id="6862" href="Data.Graph.Acyclic.html#weaken" class="Function">weaken</a> <a id="6869" class="Symbol">{</a><a id="6870" href="Data.Graph.Acyclic.html#6870" class="Bound">n</a><a id="6871" class="Symbol">}</a> <a id="6873" class="Symbol">{</a><a id="6874" href="Data.Graph.Acyclic.html#6874" class="Bound">i</a><a id="6875" class="Symbol">}</a> <a id="6877" href="Data.Graph.Acyclic.html#6877" class="Bound">j</a> <a id="6879" class="Symbol">=</a> <a id="6881" href="Data.Fin.html#inject%E2%89%A4" class="Function">Fin.inject≤</a> <a id="6893" href="Data.Graph.Acyclic.html#6877" class="Bound">j</a> <a id="6895" class="Symbol">(</a><a id="6896" href="Data.Fin.Properties.html#n%E2%84%95-%E2%84%95i%E2%89%A4n" class="Function">FP.nℕ-ℕi≤n</a> <a id="6907" href="Data.Graph.Acyclic.html#6870" class="Bound">n</a> <a id="6909" class="Symbol">(</a><a id="6910" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="6914" href="Data.Graph.Acyclic.html#6874" class="Bound">i</a><a id="6915" class="Symbol">))</a>

<a id="6919" class="Comment">-- Labels each node with its node number.</a>

<a id="number" href="Data.Graph.Acyclic.html#number" class="Function">number</a> <a id="6969" class="Symbol">:</a> <a id="6971" class="Symbol">∀</a> <a id="6973" class="Symbol">{</a><a id="6974" href="Data.Graph.Acyclic.html#6974" class="Bound">N</a> <a id="6976" href="Data.Graph.Acyclic.html#6976" class="Bound">E</a> <a id="6978" href="Data.Graph.Acyclic.html#6978" class="Bound">n</a><a id="6979" class="Symbol">}</a> <a id="6981" class="Symbol">→</a> <a id="6983" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="6989" href="Data.Graph.Acyclic.html#6974" class="Bound">N</a> <a id="6991" href="Data.Graph.Acyclic.html#6976" class="Bound">E</a> <a id="6993" href="Data.Graph.Acyclic.html#6978" class="Bound">n</a> <a id="6995" class="Symbol">→</a> <a id="6997" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="7003" class="Symbol">(</a><a id="7004" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="7008" href="Data.Graph.Acyclic.html#6978" class="Bound">n</a> <a id="7010" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="7012" href="Data.Graph.Acyclic.html#6974" class="Bound">N</a><a id="7013" class="Symbol">)</a> <a id="7015" href="Data.Graph.Acyclic.html#6976" class="Bound">E</a> <a id="7017" href="Data.Graph.Acyclic.html#6978" class="Bound">n</a>
<a id="7019" href="Data.Graph.Acyclic.html#number" class="Function">number</a> <a id="7026" class="Symbol">{</a><a id="7027" href="Data.Graph.Acyclic.html#7027" class="Bound">N</a><a id="7028" class="Symbol">}</a> <a id="7030" class="Symbol">{</a><a id="7031" href="Data.Graph.Acyclic.html#7031" class="Bound">E</a><a id="7032" class="Symbol">}</a> <a id="7034" class="Symbol">=</a>
  <a id="7038" href="Data.Graph.Acyclic.html#foldr" class="Function">foldr</a> <a id="7044" class="Symbol">(λ</a> <a id="7047" href="Data.Graph.Acyclic.html#7047" class="Bound">n</a> <a id="7049" class="Symbol">→</a> <a id="7051" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="7057" class="Symbol">(</a><a id="7058" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="7062" href="Data.Graph.Acyclic.html#7047" class="Bound">n</a> <a id="7064" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="7066" href="Data.Graph.Acyclic.html#7027" class="Bound">N</a><a id="7067" class="Symbol">)</a> <a id="7069" href="Data.Graph.Acyclic.html#7031" class="Bound">E</a> <a id="7071" href="Data.Graph.Acyclic.html#7047" class="Bound">n</a><a id="7072" class="Symbol">)</a>
        <a id="7082" class="Symbol">(λ</a> <a id="7085" href="Data.Graph.Acyclic.html#7085" class="Bound">c</a> <a id="7087" href="Data.Graph.Acyclic.html#7087" class="Bound">g</a> <a id="7089" class="Symbol">→</a> <a id="7091" href="Data.Graph.Acyclic.html#cmap" class="Function">cmap</a> <a id="7096" class="Symbol">(</a><a id="7097" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">_,_</a> <a id="7101" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a><a id="7105" class="Symbol">)</a> <a id="7107" href="Function.html#id" class="Function">id</a> <a id="7110" href="Data.Graph.Acyclic.html#7085" class="Bound">c</a> <a id="7112" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="7114" href="Data.Graph.Acyclic.html#nmap" class="Function">nmap</a> <a id="7119" class="Symbol">(</a><a id="7120" href="Data.Product.html#map" class="Function">Prod.map</a> <a id="7129" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="7133" href="Function.html#id" class="Function">id</a><a id="7135" class="Symbol">)</a> <a id="7137" href="Data.Graph.Acyclic.html#7087" class="Bound">g</a><a id="7138" class="Symbol">)</a>
        <a id="7148" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a>

<a id="7151" class="Keyword">private</a>

  <a id="test-number" href="Data.Graph.Acyclic.html#test-number" class="Function">test-number</a> <a id="7174" class="Symbol">:</a> <a id="7176" href="Data.Graph.Acyclic.html#number" class="Function">number</a> <a id="7183" href="Data.Graph.Acyclic.html#example" class="Function">example</a> <a id="7191" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a>
                <a id="7209" class="Symbol">(</a><a id="7210" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="7218" class="Symbol">(</a><a id="7219" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="7221" class="Number">0</a> <a id="7223" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="7225" class="Number">0</a><a id="7226" class="Symbol">)</a> <a id="7228" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a> <a id="7231" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a>
                 <a id="7250" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="7258" class="Symbol">(</a><a id="7259" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="7261" class="Number">1</a> <a id="7263" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="7265" class="Number">1</a><a id="7266" class="Symbol">)</a> <a id="7268" class="Symbol">((</a><a id="7270" class="Number">10</a> <a id="7273" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="7275" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="7277" class="Number">1</a><a id="7278" class="Symbol">)</a> <a id="7280" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="7282" class="Symbol">(</a><a id="7283" class="Number">11</a> <a id="7286" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="7288" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="7290" class="Number">1</a><a id="7291" class="Symbol">)</a> <a id="7293" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="7295" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a><a id="7297" class="Symbol">)</a> <a id="7299" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a>
                 <a id="7318" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="7326" class="Symbol">(</a><a id="7327" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="7329" class="Number">2</a> <a id="7331" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="7333" class="Number">2</a><a id="7334" class="Symbol">)</a> <a id="7336" class="Symbol">((</a><a id="7338" class="Number">12</a> <a id="7341" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="7343" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="7345" class="Number">0</a><a id="7346" class="Symbol">)</a> <a id="7348" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="7350" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a><a id="7352" class="Symbol">)</a> <a id="7354" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a>
                 <a id="7373" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="7381" class="Symbol">(</a><a id="7382" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="7384" class="Number">3</a> <a id="7386" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="7388" class="Number">3</a><a id="7389" class="Symbol">)</a> <a id="7391" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a> <a id="7394" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a>
                 <a id="7413" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="7421" class="Symbol">(</a><a id="7422" href="Data.Fin.html#%23_" class="Function Operator">#</a> <a id="7424" class="Number">4</a> <a id="7426" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="7428" class="Number">4</a><a id="7429" class="Symbol">)</a> <a id="7431" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a> <a id="7434" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a>
                 <a id="7453" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a><a id="7454" class="Symbol">)</a>
  <a id="7458" href="Data.Graph.Acyclic.html#test-number" class="Function">test-number</a> <a id="7470" class="Symbol">=</a> <a id="7472" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a>

<a id="7480" class="Comment">-- Reverses all the edges in the graph.</a>

<a id="reverse" href="Data.Graph.Acyclic.html#reverse" class="Function">reverse</a> <a id="7529" class="Symbol">:</a> <a id="7531" class="Symbol">∀</a> <a id="7533" class="Symbol">{</a><a id="7534" href="Data.Graph.Acyclic.html#7534" class="Bound">N</a> <a id="7536" href="Data.Graph.Acyclic.html#7536" class="Bound">E</a> <a id="7538" href="Data.Graph.Acyclic.html#7538" class="Bound">n</a><a id="7539" class="Symbol">}</a> <a id="7541" class="Symbol">→</a> <a id="7543" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="7549" href="Data.Graph.Acyclic.html#7534" class="Bound">N</a> <a id="7551" href="Data.Graph.Acyclic.html#7536" class="Bound">E</a> <a id="7553" href="Data.Graph.Acyclic.html#7538" class="Bound">n</a> <a id="7555" class="Symbol">→</a> <a id="7557" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="7563" href="Data.Graph.Acyclic.html#7534" class="Bound">N</a> <a id="7565" href="Data.Graph.Acyclic.html#7536" class="Bound">E</a> <a id="7567" href="Data.Graph.Acyclic.html#7538" class="Bound">n</a>
<a id="7569" href="Data.Graph.Acyclic.html#reverse" class="Function">reverse</a> <a id="7577" class="Symbol">{</a><a id="7578" href="Data.Graph.Acyclic.html#7578" class="Bound">N</a><a id="7579" class="Symbol">}</a> <a id="7581" class="Symbol">{</a><a id="7582" href="Data.Graph.Acyclic.html#7582" class="Bound">E</a><a id="7583" class="Symbol">}</a> <a id="7585" href="Data.Graph.Acyclic.html#7585" class="Bound">g</a> <a id="7587" class="Symbol">=</a>
  <a id="7591" href="Data.Graph.Acyclic.html#foldl" class="Function">foldl</a> <a id="7597" class="Symbol">(</a><a id="7598" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="7604" href="Data.Graph.Acyclic.html#7578" class="Bound">N</a> <a id="7606" href="Data.Graph.Acyclic.html#7582" class="Bound">E</a><a id="7607" class="Symbol">)</a>
        <a id="7617" class="Symbol">(λ</a> <a id="7620" href="Data.Graph.Acyclic.html#7620" class="Bound">i</a> <a id="7622" href="Data.Graph.Acyclic.html#7622" class="Bound">g&#39;</a> <a id="7625" href="Data.Graph.Acyclic.html#7625" class="Bound">c</a> <a id="7627" class="Symbol">→</a>
           <a id="7640" href="Data.Graph.Acyclic.html#Context.context" class="InductiveConstructor">context</a> <a id="7648" class="Symbol">(</a><a id="7649" href="Data.Graph.Acyclic.html#Context.label" class="Field">label</a> <a id="7655" href="Data.Graph.Acyclic.html#7625" class="Bound">c</a><a id="7656" class="Symbol">)</a>
                   <a id="7677" class="Symbol">(</a><a id="7678" href="Data.List.Base.html#map" class="Function">List.map</a> <a id="7687" class="Symbol">(</a><a id="7688" href="Data.Product.html#swap" class="Function">Prod.swap</a> <a id="7698" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="7700" href="Data.Product.html#map" class="Function">Prod.map</a> <a id="7709" href="Data.Fin.Properties.html#reverse" class="Function">FP.reverse</a> <a id="7720" href="Function.html#id" class="Function">id</a><a id="7722" class="Symbol">)</a> <a id="7724" href="Function.html#_%24_" class="Function Operator">$</a>
                             <a id="7755" href="Data.Graph.Acyclic.html#preds" class="Function">preds</a> <a id="7761" href="Data.Graph.Acyclic.html#7585" class="Bound">g</a> <a id="7763" href="Data.Graph.Acyclic.html#7620" class="Bound">i</a><a id="7764" class="Symbol">)</a>
           <a id="7777" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="7779" href="Data.Graph.Acyclic.html#7622" class="Bound">g&#39;</a><a id="7781" class="Symbol">)</a>
        <a id="7791" href="Data.Graph.Acyclic.html#Graph.%E2%88%85" class="InductiveConstructor">∅</a> <a id="7793" href="Data.Graph.Acyclic.html#7585" class="Bound">g</a>

<a id="7796" class="Keyword">private</a>

  <a id="test-reverse" href="Data.Graph.Acyclic.html#test-reverse" class="Function">test-reverse</a> <a id="7820" class="Symbol">:</a> <a id="7822" href="Data.Graph.Acyclic.html#reverse" class="Function">reverse</a> <a id="7830" class="Symbol">(</a><a id="7831" href="Data.Graph.Acyclic.html#reverse" class="Function">reverse</a> <a id="7839" href="Data.Graph.Acyclic.html#example" class="Function">example</a><a id="7846" class="Symbol">)</a> <a id="7848" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="7850" href="Data.Graph.Acyclic.html#example" class="Function">example</a>
  <a id="7860" href="Data.Graph.Acyclic.html#test-reverse" class="Function">test-reverse</a> <a id="7873" class="Symbol">=</a> <a id="7875" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a>

<a id="7883" class="Comment">------------------------------------------------------------------------</a>
<a id="7956" class="Comment">-- Views</a>

<a id="7966" class="Comment">-- Expands the subgraph induced by a given node into a tree (thus</a>
<a id="8032" class="Comment">-- losing all sharing).</a>

<a id="8057" class="Keyword">data</a> <a id="Tree" href="Data.Graph.Acyclic.html#Tree" class="Datatype">Tree</a> <a id="8067" class="Symbol">(</a><a id="8068" href="Data.Graph.Acyclic.html#8068" class="Bound">N</a> <a id="8070" href="Data.Graph.Acyclic.html#8070" class="Bound">E</a> <a id="8072" class="Symbol">:</a> <a id="8074" class="PrimitiveType">Set</a><a id="8077" class="Symbol">)</a> <a id="8079" class="Symbol">:</a> <a id="8081" class="PrimitiveType">Set</a> <a id="8085" class="Keyword">where</a>
  <a id="Tree.node" href="Data.Graph.Acyclic.html#Tree.node" class="InductiveConstructor">node</a> <a id="8098" class="Symbol">:</a> <a id="8100" class="Symbol">(</a><a id="8101" href="Data.Graph.Acyclic.html#8101" class="Bound">label</a> <a id="8107" class="Symbol">:</a> <a id="8109" href="Data.Graph.Acyclic.html#8068" class="Bound">N</a><a id="8110" class="Symbol">)</a> <a id="8112" class="Symbol">(</a><a id="8113" href="Data.Graph.Acyclic.html#8113" class="Bound">successors</a> <a id="8124" class="Symbol">:</a> <a id="8126" href="Agda.Builtin.List.html#List" class="Datatype">List</a> <a id="8131" class="Symbol">(</a><a id="8132" href="Data.Graph.Acyclic.html#8070" class="Bound">E</a> <a id="8134" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="8136" href="Data.Graph.Acyclic.html#Tree" class="Datatype">Tree</a> <a id="8141" href="Data.Graph.Acyclic.html#8068" class="Bound">N</a> <a id="8143" href="Data.Graph.Acyclic.html#8070" class="Bound">E</a><a id="8144" class="Symbol">))</a> <a id="8147" class="Symbol">→</a> <a id="8149" href="Data.Graph.Acyclic.html#Tree" class="Datatype">Tree</a> <a id="8154" href="Data.Graph.Acyclic.html#8068" class="Bound">N</a> <a id="8156" href="Data.Graph.Acyclic.html#8070" class="Bound">E</a>

<a id="toTree" href="Data.Graph.Acyclic.html#toTree" class="Function">toTree</a> <a id="8166" class="Symbol">:</a> <a id="8168" class="Symbol">∀</a> <a id="8170" class="Symbol">{</a><a id="8171" href="Data.Graph.Acyclic.html#8171" class="Bound">N</a> <a id="8173" href="Data.Graph.Acyclic.html#8173" class="Bound">E</a> <a id="8175" href="Data.Graph.Acyclic.html#8175" class="Bound">n</a><a id="8176" class="Symbol">}</a> <a id="8178" class="Symbol">→</a> <a id="8180" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="8186" href="Data.Graph.Acyclic.html#8171" class="Bound">N</a> <a id="8188" href="Data.Graph.Acyclic.html#8173" class="Bound">E</a> <a id="8190" href="Data.Graph.Acyclic.html#8175" class="Bound">n</a> <a id="8192" class="Symbol">→</a> <a id="8194" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="8198" href="Data.Graph.Acyclic.html#8175" class="Bound">n</a> <a id="8200" class="Symbol">→</a> <a id="8202" href="Data.Graph.Acyclic.html#Tree" class="Datatype">Tree</a> <a id="8207" href="Data.Graph.Acyclic.html#8171" class="Bound">N</a> <a id="8209" href="Data.Graph.Acyclic.html#8173" class="Bound">E</a>
<a id="8211" href="Data.Graph.Acyclic.html#toTree" class="Function">toTree</a> <a id="8218" class="Symbol">{</a><a id="8219" href="Data.Graph.Acyclic.html#8219" class="Bound">N</a><a id="8220" class="Symbol">}</a> <a id="8222" class="Symbol">{</a><a id="8223" href="Data.Graph.Acyclic.html#8223" class="Bound">E</a><a id="8224" class="Symbol">}</a> <a id="8226" href="Data.Graph.Acyclic.html#8226" class="Bound">g</a> <a id="8228" href="Data.Graph.Acyclic.html#8228" class="Bound">i</a> <a id="8230" class="Symbol">=</a> <a id="8232" href="Induction.WellFounded.html#1751" class="Function">&lt;′-rec</a> <a id="8239" href="Data.Graph.Acyclic.html#8273" class="Function">Pred</a> <a id="8244" href="Data.Graph.Acyclic.html#8318" class="Function">expand</a> <a id="8251" class="Symbol">_</a> <a id="8253" class="Symbol">(</a><a id="8254" href="Data.Graph.Acyclic.html#8226" class="Bound">g</a> <a id="8256" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">[</a> <a id="8258" href="Data.Graph.Acyclic.html#8228" class="Bound">i</a> <a id="8260" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">]</a><a id="8261" class="Symbol">)</a>
  <a id="8265" class="Keyword">where</a>
  <a id="8273" href="Data.Graph.Acyclic.html#8273" class="Function">Pred</a> <a id="8278" class="Symbol">=</a> <a id="8280" class="Symbol">λ</a> <a id="8282" href="Data.Graph.Acyclic.html#8282" class="Bound">n</a> <a id="8284" class="Symbol">→</a> <a id="8286" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="8292" href="Data.Graph.Acyclic.html#8219" class="Bound">N</a> <a id="8294" href="Data.Graph.Acyclic.html#8223" class="Bound">E</a> <a id="8296" class="Symbol">(</a><a id="8297" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="8301" href="Data.Graph.Acyclic.html#8282" class="Bound">n</a><a id="8302" class="Symbol">)</a> <a id="8304" class="Symbol">→</a> <a id="8306" href="Data.Graph.Acyclic.html#Tree" class="Datatype">Tree</a> <a id="8311" href="Data.Graph.Acyclic.html#8219" class="Bound">N</a> <a id="8313" href="Data.Graph.Acyclic.html#8223" class="Bound">E</a>

  <a id="8318" href="Data.Graph.Acyclic.html#8318" class="Function">expand</a> <a id="8325" class="Symbol">:</a> <a id="8327" class="Symbol">(</a><a id="8328" href="Data.Graph.Acyclic.html#8328" class="Bound">n</a> <a id="8330" class="Symbol">:</a> <a id="8332" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="8333" class="Symbol">)</a> <a id="8335" class="Symbol">→</a> <a id="8337" href="Induction.Nat.html#%3C%E2%80%B2-Rec" class="Function">&lt;′-Rec</a> <a id="8344" href="Data.Graph.Acyclic.html#8273" class="Function">Pred</a> <a id="8349" href="Data.Graph.Acyclic.html#8328" class="Bound">n</a> <a id="8351" class="Symbol">→</a> <a id="8353" href="Data.Graph.Acyclic.html#8273" class="Function">Pred</a> <a id="8358" href="Data.Graph.Acyclic.html#8328" class="Bound">n</a>
  <a id="8362" href="Data.Graph.Acyclic.html#8318" class="Function">expand</a> <a id="8369" href="Data.Graph.Acyclic.html#8369" class="Bound">n</a> <a id="8371" href="Data.Graph.Acyclic.html#8371" class="Bound">rec</a> <a id="8375" class="Symbol">(</a><a id="8376" href="Data.Graph.Acyclic.html#8376" class="Bound">c</a> <a id="8378" href="Data.Graph.Acyclic.html#Graph._%26_" class="InductiveConstructor Operator">&amp;</a> <a id="8380" href="Data.Graph.Acyclic.html#8380" class="Bound">g</a><a id="8381" class="Symbol">)</a> <a id="8383" class="Symbol">=</a>
    <a id="8389" href="Data.Graph.Acyclic.html#Tree.node" class="InductiveConstructor">node</a> <a id="8394" class="Symbol">(</a><a id="8395" href="Data.Graph.Acyclic.html#Context.label" class="Field">label</a> <a id="8401" href="Data.Graph.Acyclic.html#8376" class="Bound">c</a><a id="8402" class="Symbol">)</a>
         <a id="8413" class="Symbol">(</a><a id="8414" href="Data.List.Base.html#map" class="Function">List.map</a>
            <a id="8435" class="Symbol">(</a><a id="8436" href="Data.Product.html#map" class="Function">Prod.map</a> <a id="8445" href="Function.html#id" class="Function">id</a> <a id="8448" class="Symbol">(λ</a> <a id="8451" href="Data.Graph.Acyclic.html#8451" class="Bound">i</a> <a id="8453" class="Symbol">→</a> <a id="8455" href="Data.Graph.Acyclic.html#8371" class="Bound">rec</a> <a id="8459" class="Symbol">(</a><a id="8460" href="Data.Graph.Acyclic.html#8369" class="Bound">n</a> <a id="8462" href="Data.Fin.html#_-_" class="Function Operator">-</a> <a id="8464" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="8468" href="Data.Graph.Acyclic.html#8451" class="Bound">i</a><a id="8469" class="Symbol">)</a> <a id="8471" class="Symbol">(</a><a id="8472" href="Data.Graph.Acyclic.html#lemma" class="Function">lemma</a> <a id="8478" href="Data.Graph.Acyclic.html#8369" class="Bound">n</a> <a id="8480" href="Data.Graph.Acyclic.html#8451" class="Bound">i</a><a id="8481" class="Symbol">)</a> <a id="8483" class="Symbol">(</a><a id="8484" href="Data.Graph.Acyclic.html#8380" class="Bound">g</a> <a id="8486" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">[</a> <a id="8488" href="Data.Graph.Acyclic.html#8451" class="Bound">i</a> <a id="8490" href="Data.Graph.Acyclic.html#_%5B_%5D" class="Function Operator">]</a><a id="8491" class="Symbol">)))</a>
            <a id="8507" class="Symbol">(</a><a id="8508" href="Data.Graph.Acyclic.html#Context.successors" class="Field">successors</a> <a id="8519" href="Data.Graph.Acyclic.html#8376" class="Bound">c</a><a id="8520" class="Symbol">))</a>

<a id="8524" class="Comment">-- Performs the toTree expansion once for each node.</a>

<a id="toForest" href="Data.Graph.Acyclic.html#toForest" class="Function">toForest</a> <a id="8587" class="Symbol">:</a> <a id="8589" class="Symbol">∀</a> <a id="8591" class="Symbol">{</a><a id="8592" href="Data.Graph.Acyclic.html#8592" class="Bound">N</a> <a id="8594" href="Data.Graph.Acyclic.html#8594" class="Bound">E</a> <a id="8596" href="Data.Graph.Acyclic.html#8596" class="Bound">n</a><a id="8597" class="Symbol">}</a> <a id="8599" class="Symbol">→</a> <a id="8601" href="Data.Graph.Acyclic.html#Graph" class="Datatype">Graph</a> <a id="8607" href="Data.Graph.Acyclic.html#8592" class="Bound">N</a> <a id="8609" href="Data.Graph.Acyclic.html#8594" class="Bound">E</a> <a id="8611" href="Data.Graph.Acyclic.html#8596" class="Bound">n</a> <a id="8613" class="Symbol">→</a> <a id="8615" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="8619" class="Symbol">(</a><a id="8620" href="Data.Graph.Acyclic.html#Tree" class="Datatype">Tree</a> <a id="8625" href="Data.Graph.Acyclic.html#8592" class="Bound">N</a> <a id="8627" href="Data.Graph.Acyclic.html#8594" class="Bound">E</a><a id="8628" class="Symbol">)</a> <a id="8630" href="Data.Graph.Acyclic.html#8596" class="Bound">n</a>
<a id="8632" href="Data.Graph.Acyclic.html#toForest" class="Function">toForest</a> <a id="8641" href="Data.Graph.Acyclic.html#8641" class="Bound">g</a> <a id="8643" class="Symbol">=</a> <a id="8645" href="Data.Vec.html#map" class="Function">Vec.map</a> <a id="8653" class="Symbol">(</a><a id="8654" href="Data.Graph.Acyclic.html#toTree" class="Function">toTree</a> <a id="8661" href="Data.Graph.Acyclic.html#8641" class="Bound">g</a><a id="8662" class="Symbol">)</a> <a id="8664" class="Symbol">(</a><a id="8665" href="Data.Vec.html#allFin" class="Function">Vec.allFin</a> <a id="8676" class="Symbol">_)</a>

<a id="8680" class="Keyword">private</a>

  <a id="test-toForest" href="Data.Graph.Acyclic.html#test-toForest" class="Function">test-toForest</a> <a id="8705" class="Symbol">:</a> <a id="8707" href="Data.Graph.Acyclic.html#toForest" class="Function">toForest</a> <a id="8716" href="Data.Graph.Acyclic.html#example" class="Function">example</a> <a id="8724" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a>
                    <a id="8746" class="Keyword">let</a> <a id="8750" href="Data.Graph.Acyclic.html#8750" class="Bound">n3</a> <a id="8753" class="Symbol">=</a> <a id="8755" href="Data.Graph.Acyclic.html#Tree.node" class="InductiveConstructor">node</a> <a id="8760" class="Number">3</a> <a id="8762" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a> <a id="8765" class="Keyword">in</a>
                    <a id="8788" href="Data.Graph.Acyclic.html#Tree.node" class="InductiveConstructor">node</a> <a id="8793" class="Number">0</a> <a id="8795" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a> <a id="8798" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a>
                    <a id="8820" href="Data.Graph.Acyclic.html#Tree.node" class="InductiveConstructor">node</a> <a id="8825" class="Number">1</a> <a id="8827" class="Symbol">((</a><a id="8829" class="Number">10</a> <a id="8832" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="8834" href="Data.Graph.Acyclic.html#8750" class="Bound">n3</a><a id="8836" class="Symbol">)</a> <a id="8838" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="8840" class="Symbol">(</a><a id="8841" class="Number">11</a> <a id="8844" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="8846" href="Data.Graph.Acyclic.html#8750" class="Bound">n3</a><a id="8848" class="Symbol">)</a> <a id="8850" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="8852" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a><a id="8854" class="Symbol">)</a> <a id="8856" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a>
                    <a id="8878" href="Data.Graph.Acyclic.html#Tree.node" class="InductiveConstructor">node</a> <a id="8883" class="Number">2</a> <a id="8885" class="Symbol">((</a><a id="8887" class="Number">12</a> <a id="8890" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="8892" href="Data.Graph.Acyclic.html#8750" class="Bound">n3</a><a id="8894" class="Symbol">)</a> <a id="8896" href="Agda.Builtin.List.html#List._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="8898" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a><a id="8900" class="Symbol">)</a> <a id="8902" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a>
                    <a id="8924" href="Data.Graph.Acyclic.html#Tree.node" class="InductiveConstructor">node</a> <a id="8929" class="Number">3</a> <a id="8931" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a> <a id="8934" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a>
                    <a id="8956" href="Data.Graph.Acyclic.html#Tree.node" class="InductiveConstructor">node</a> <a id="8961" class="Number">4</a> <a id="8963" href="Agda.Builtin.List.html#List.%5B%5D" class="InductiveConstructor">[]</a> <a id="8966" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a>
                    <a id="8988" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a>
  <a id="8993" href="Data.Graph.Acyclic.html#test-toForest" class="Function">test-toForest</a> <a id="9007" class="Symbol">=</a> <a id="9009" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a>
</pre></body></html>

APT Browse - Built by Thomas Orozco.