|
22 | 22 | <a id="853" class="Keyword">open</a> <a id="858" class="Keyword">import</a> <a id="865" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a> <a id="879" class="Keyword">using</a> <a id="885" class="Symbol">(</a><a id="886" href="Data.Sum.Base.html#625" class="Datatype Operator">_⊎_</a><a id="889" class="Symbol">;</a> <a id="891" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a><a id="895" class="Symbol">;</a> <a id="897" href="Data.Sum.Base.html#700" class="InductiveConstructor">inj₂</a><a id="901" class="Symbol">;</a> <a id="903" href="Data.Sum.Base.html#811" class="Function Operator">[_,_]</a><a id="908" class="Symbol">)</a> |
23 | 23 | <a id="910" class="Keyword">open</a> <a id="915" class="Keyword">import</a> <a id="922" href="Function.Base.html" class="Module">Function.Base</a> <a id="936" class="Keyword">using</a> <a id="942" class="Symbol">(</a><a id="943" href="Function.Base.html#4322" class="Function Operator">_⟨_⟩_</a><a id="948" class="Symbol">;</a> <a id="950" href="Function.Base.html#725" class="Function">const</a><a id="955" class="Symbol">;</a> <a id="957" href="Function.Base.html#704" class="Function">id</a><a id="959" class="Symbol">)</a> |
24 | 24 | <a id="961" class="Keyword">open</a> <a id="966" class="Keyword">import</a> <a id="973" href="Function.Bundles.html" class="Module">Function.Bundles</a> <a id="990" class="Keyword">hiding</a> <a id="997" class="Symbol">(</a><a id="998" href="Function.Bundles.html#7340" class="Record">Inverse</a><a id="1005" class="Symbol">;</a> <a id="1007" href="Function.Bundles.html#5375" class="Record">LeftInverse</a><a id="1018" class="Symbol">;</a> <a id="1020" href="Function.Bundles.html#6509" class="Record">RightInverse</a><a id="1032" class="Symbol">)</a> |
25 | | -<a id="1034" class="Keyword">open</a> <a id="1039" class="Keyword">import</a> <a id="1046" href="Induction.WellFounded.html" class="Module">Induction.WellFounded</a> <a id="1068" class="Keyword">using</a> <a id="1074" class="Symbol">(</a><a id="1075" href="Induction.WellFounded.html#1356" class="Datatype">Acc</a><a id="1078" class="Symbol">;</a> <a id="1080" href="Induction.WellFounded.html#1604" class="Function">WellFounded</a><a id="1091" class="Symbol">;</a> <a id="1093" href="Induction.WellFounded.html#1418" class="InductiveConstructor">acc</a><a id="1096" class="Symbol">)</a> |
| 25 | +<a id="1034" class="Keyword">open</a> <a id="1039" class="Keyword">import</a> <a id="1046" href="Induction.WellFounded.html" class="Module">Induction.WellFounded</a> <a id="1068" class="Keyword">using</a> <a id="1074" class="Symbol">(</a><a id="1075" href="Induction.WellFounded.html#1545" class="Datatype">Acc</a><a id="1078" class="Symbol">;</a> <a id="1080" href="Induction.WellFounded.html#1793" class="Function">WellFounded</a><a id="1091" class="Symbol">;</a> <a id="1093" href="Induction.WellFounded.html#1607" class="InductiveConstructor">acc</a><a id="1096" class="Symbol">)</a> |
26 | 26 | <a id="1098" class="Keyword">open</a> <a id="1103" class="Keyword">import</a> <a id="1110" href="Level.html" class="Module">Level</a> <a id="1116" class="Keyword">using</a> <a id="1122" class="Symbol">(</a><a id="1123" href="Level.html#521" class="Function">0ℓ</a><a id="1125" class="Symbol">;</a> <a id="1127" href="Agda.Primitive.html#742" class="Postulate">Level</a><a id="1132" class="Symbol">)</a> |
27 | 27 | <a id="1134" class="Keyword">open</a> <a id="1139" class="Keyword">import</a> <a id="1146" href="Relation.Binary.Bundles.html" class="Module">Relation.Binary.Bundles</a> <a id="1170" class="Keyword">using</a> <a id="1176" class="Symbol">(</a><a id="1177" href="Relation.Binary.Bundles.html#1672" class="Record">DecSetoid</a><a id="1186" class="Symbol">;</a> <a id="1188" href="Relation.Binary.Bundles.html#8129" class="Record">DecTotalOrder</a><a id="1201" class="Symbol">;</a> <a id="1203" href="Relation.Binary.Bundles.html#4418" class="Record">Poset</a><a id="1208" class="Symbol">;</a> |
28 | 28 | <a id="1212" href="Relation.Binary.Bundles.html#2245" class="Record">Preorder</a><a id="1220" class="Symbol">;</a> <a id="1222" href="Relation.Binary.Bundles.html#1204" class="Record">Setoid</a><a id="1228" class="Symbol">;</a> <a id="1230" href="Relation.Binary.Bundles.html#5841" class="Record">StrictPartialOrder</a><a id="1248" class="Symbol">;</a> <a id="1250" href="Relation.Binary.Bundles.html#9119" class="Record">StrictTotalOrder</a><a id="1266" class="Symbol">;</a> <a id="1268" href="Relation.Binary.Bundles.html#7546" class="Record">TotalOrder</a><a id="1278" class="Symbol">)</a> |
|
205 | 205 | <a id="<-irrelevant"></a><a id="5389" href="Data.Bool.Properties.html#5389" class="Function"><-irrelevant</a> <a id="5402" class="Symbol">:</a> <a id="5404" href="Relation.Binary.Definitions.html#6066" class="Function">Irrelevant</a> <a id="5415" href="Data.Bool.Base.html#770" class="Datatype Operator">_<_</a> |
206 | 206 | <a id="5419" href="Data.Bool.Properties.html#5389" class="Function"><-irrelevant</a> <a id="5432" href="Data.Bool.Base.html#802" class="InductiveConstructor">f<t</a> <a id="5436" href="Data.Bool.Base.html#802" class="InductiveConstructor">f<t</a> <a id="5440" class="Symbol">=</a> <a id="5442" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> |
207 | 207 |
|
208 | | -<a id="<-wellFounded"></a><a id="5448" href="Data.Bool.Properties.html#5448" class="Function"><-wellFounded</a> <a id="5462" class="Symbol">:</a> <a id="5464" href="Induction.WellFounded.html#1604" class="Function">WellFounded</a> <a id="5476" href="Data.Bool.Base.html#770" class="Datatype Operator">_<_</a> |
209 | | -<a id="5480" href="Data.Bool.Properties.html#5448" class="Function"><-wellFounded</a> <a id="5494" class="Symbol">_</a> <a id="5496" class="Symbol">=</a> <a id="5498" href="Induction.WellFounded.html#1418" class="InductiveConstructor">acc</a> <a id="5502" href="Data.Bool.Properties.html#5520" class="Function"><-acc</a> |
| 208 | +<a id="<-wellFounded"></a><a id="5448" href="Data.Bool.Properties.html#5448" class="Function"><-wellFounded</a> <a id="5462" class="Symbol">:</a> <a id="5464" href="Induction.WellFounded.html#1793" class="Function">WellFounded</a> <a id="5476" href="Data.Bool.Base.html#770" class="Datatype Operator">_<_</a> |
| 209 | +<a id="5480" href="Data.Bool.Properties.html#5448" class="Function"><-wellFounded</a> <a id="5494" class="Symbol">_</a> <a id="5496" class="Symbol">=</a> <a id="5498" href="Induction.WellFounded.html#1607" class="InductiveConstructor">acc</a> <a id="5502" href="Data.Bool.Properties.html#5520" class="Function"><-acc</a> |
210 | 210 | <a id="5510" class="Keyword">where</a> |
211 | | - <a id="5520" href="Data.Bool.Properties.html#5520" class="Function"><-acc</a> <a id="5526" class="Symbol">:</a> <a id="5528" class="Symbol">∀</a> <a id="5530" class="Symbol">{</a><a id="5531" href="Data.Bool.Properties.html#5531" class="Bound">x</a> <a id="5533" href="Data.Bool.Properties.html#5533" class="Bound">y</a><a id="5534" class="Symbol">}</a> <a id="5536" class="Symbol">→</a> <a id="5538" href="Data.Bool.Properties.html#5533" class="Bound">y</a> <a id="5540" href="Data.Bool.Base.html#770" class="Datatype Operator"><</a> <a id="5542" href="Data.Bool.Properties.html#5531" class="Bound">x</a> <a id="5544" class="Symbol">→</a> <a id="5546" href="Induction.WellFounded.html#1356" class="Datatype">Acc</a> <a id="5550" href="Data.Bool.Base.html#770" class="Datatype Operator">_<_</a> <a id="5554" href="Data.Bool.Properties.html#5533" class="Bound">y</a> |
212 | | - <a id="5560" href="Data.Bool.Properties.html#5520" class="Function"><-acc</a> <a id="5566" href="Data.Bool.Base.html#802" class="InductiveConstructor">f<t</a> <a id="5570" class="Symbol">=</a> <a id="5572" href="Induction.WellFounded.html#1418" class="InductiveConstructor">acc</a> <a id="5576" class="Symbol">λ</a> <a id="5578" class="Symbol">()</a> |
| 211 | + <a id="5520" href="Data.Bool.Properties.html#5520" class="Function"><-acc</a> <a id="5526" class="Symbol">:</a> <a id="5528" class="Symbol">∀</a> <a id="5530" class="Symbol">{</a><a id="5531" href="Data.Bool.Properties.html#5531" class="Bound">x</a> <a id="5533" href="Data.Bool.Properties.html#5533" class="Bound">y</a><a id="5534" class="Symbol">}</a> <a id="5536" class="Symbol">→</a> <a id="5538" href="Data.Bool.Properties.html#5533" class="Bound">y</a> <a id="5540" href="Data.Bool.Base.html#770" class="Datatype Operator"><</a> <a id="5542" href="Data.Bool.Properties.html#5531" class="Bound">x</a> <a id="5544" class="Symbol">→</a> <a id="5546" href="Induction.WellFounded.html#1545" class="Datatype">Acc</a> <a id="5550" href="Data.Bool.Base.html#770" class="Datatype Operator">_<_</a> <a id="5554" href="Data.Bool.Properties.html#5533" class="Bound">y</a> |
| 212 | + <a id="5560" href="Data.Bool.Properties.html#5520" class="Function"><-acc</a> <a id="5566" href="Data.Bool.Base.html#802" class="InductiveConstructor">f<t</a> <a id="5570" class="Symbol">=</a> <a id="5572" href="Induction.WellFounded.html#1607" class="InductiveConstructor">acc</a> <a id="5576" class="Symbol">λ</a> <a id="5578" class="Symbol">()</a> |
213 | 213 |
|
214 | 214 | <a id="5582" class="Comment">-- Structures</a> |
215 | 215 |
|
|
![github-merge-queue[bot]](https://avatars.githubusercontent.com/u/9919?v=4&size=40){kind=avatar}
0 commit comments