-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathData.List.Relation.Unary.Unique.Setoid.html
30 lines (21 loc) · 5.44 KB
/
Data.List.Relation.Unary.Unique.Setoid.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Data.List.Relation.Unary.Unique.Setoid</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- Lists made up entirely of unique elements (setoid equality)</a>
<a id="169" class="Comment">------------------------------------------------------------------------</a>
<a id="243" class="Symbol">{-#</a> <a id="247" class="Keyword">OPTIONS</a> <a id="255" class="Pragma">--without-K</a> <a id="267" class="Pragma">--safe</a> <a id="274" class="Symbol">#-}</a>
<a id="279" class="Keyword">open</a> <a id="284" class="Keyword">import</a> <a id="291" href="Relation.Binary.html" class="Module">Relation.Binary</a> <a id="307" class="Keyword">using</a> <a id="313" class="Symbol">(</a><a id="314" href="Relation.Binary.Core.html#882" class="Function">Rel</a><a id="317" class="Symbol">;</a> <a id="319" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a><a id="325" class="Symbol">)</a>
<a id="327" class="Keyword">open</a> <a id="332" class="Keyword">import</a> <a id="339" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="356" class="Keyword">using</a> <a id="362" class="Symbol">(</a><a id="363" href="Relation.Nullary.html#656" class="Function Operator">¬_</a><a id="365" class="Symbol">)</a>
<a id="368" class="Keyword">module</a> <a id="375" href="Data.List.Relation.Unary.Unique.Setoid.html" class="Module">Data.List.Relation.Unary.Unique.Setoid</a> <a id="414" class="Symbol">{</a><a id="415" href="Data.List.Relation.Unary.Unique.Setoid.html#415" class="Bound">a</a> <a id="417" href="Data.List.Relation.Unary.Unique.Setoid.html#417" class="Bound">ℓ</a><a id="418" class="Symbol">}</a> <a id="420" class="Symbol">(</a><a id="421" href="Data.List.Relation.Unary.Unique.Setoid.html#421" class="Bound">S</a> <a id="423" class="Symbol">:</a> <a id="425" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="432" href="Data.List.Relation.Unary.Unique.Setoid.html#415" class="Bound">a</a> <a id="434" href="Data.List.Relation.Unary.Unique.Setoid.html#417" class="Bound">ℓ</a><a id="435" class="Symbol">)</a> <a id="437" class="Keyword">where</a>
<a id="444" class="Keyword">open</a> <a id="449" href="Relation.Binary.Bundles.html#1009" class="Module">Setoid</a> <a id="456" href="Data.List.Relation.Unary.Unique.Setoid.html#421" class="Bound">S</a> <a id="458" class="Keyword">renaming</a> <a id="467" class="Symbol">(</a><a id="468" href="Relation.Binary.Bundles.html#1072" class="Field">Carrier</a> <a id="476" class="Symbol">to</a> <a id="479" class="Field">A</a><a id="480" class="Symbol">)</a>
<a id="483" class="Comment">------------------------------------------------------------------------</a>
<a id="556" class="Comment">-- Definition</a>
<a id="571" class="Keyword">private</a>
<a id="Distinct"></a><a id="581" href="Data.List.Relation.Unary.Unique.Setoid.html#581" class="Function">Distinct</a> <a id="590" class="Symbol">:</a> <a id="592" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="596" href="Data.List.Relation.Unary.Unique.Setoid.html#479" class="Field">A</a> <a id="598" href="Data.List.Relation.Unary.Unique.Setoid.html#417" class="Bound">ℓ</a>
<a id="602" href="Data.List.Relation.Unary.Unique.Setoid.html#581" class="Function">Distinct</a> <a id="611" href="Data.List.Relation.Unary.Unique.Setoid.html#611" class="Bound">x</a> <a id="613" href="Data.List.Relation.Unary.Unique.Setoid.html#613" class="Bound">y</a> <a id="615" class="Symbol">=</a> <a id="617" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="619" class="Symbol">(</a><a id="620" href="Data.List.Relation.Unary.Unique.Setoid.html#611" class="Bound">x</a> <a id="622" href="Relation.Binary.Bundles.html#1098" class="Field Operator">≈</a> <a id="624" href="Data.List.Relation.Unary.Unique.Setoid.html#613" class="Bound">y</a><a id="625" class="Symbol">)</a>
<a id="628" class="Keyword">open</a> <a id="633" class="Keyword">import</a> <a id="640" href="Data.List.Relation.Unary.AllPairs.Core.html" class="Module">Data.List.Relation.Unary.AllPairs.Core</a> <a id="679" href="Data.List.Relation.Unary.Unique.Setoid.html#581" class="Function">Distinct</a> <a id="688" class="Keyword">public</a>
<a id="697" class="Keyword">renaming</a> <a id="706" class="Symbol">(</a><a id="707" href="Data.List.Relation.Unary.AllPairs.Core.html#941" class="Datatype">AllPairs</a> <a id="716" class="Symbol">to</a> <a id="719" class="Datatype">Unique</a><a id="725" class="Symbol">)</a>
<a id="728" class="Keyword">open</a> <a id="733" class="Keyword">import</a> <a id="740" href="Data.List.Relation.Unary.AllPairs.html" class="Module">Data.List.Relation.Unary.AllPairs</a> <a id="774" class="Symbol">{</a><a id="775" class="Argument">R</a> <a id="777" class="Symbol">=</a> <a id="779" href="Data.List.Relation.Unary.Unique.Setoid.html#581" class="Function">Distinct</a><a id="787" class="Symbol">}</a> <a id="789" class="Keyword">public</a>
<a id="798" class="Keyword">using</a> <a id="804" class="Symbol">(</a><a id="805" href="Data.List.Relation.Unary.AllPairs.html#1283" class="Function">head</a><a id="809" class="Symbol">;</a> <a id="811" href="Data.List.Relation.Unary.AllPairs.html#1358" class="Function">tail</a><a id="815" class="Symbol">)</a>
</pre></body></html>