-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathData.Char.Properties.html
319 lines (257 loc) · 61.5 KB
/
Data.Char.Properties.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
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
318
319
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Data.Char.Properties</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">-- Properties of operations on characters</a>
<a id="148" class="Comment">------------------------------------------------------------------------</a>
<a id="222" class="Symbol">{-#</a> <a id="226" class="Keyword">OPTIONS</a> <a id="234" class="Pragma">--without-K</a> <a id="246" class="Pragma">--safe</a> <a id="253" class="Symbol">#-}</a>
<a id="257" class="Symbol">{-#</a> <a id="261" class="Keyword">OPTIONS</a> <a id="269" class="Pragma">-WnoUserWarning</a> <a id="285" class="Symbol">#-}</a>
<a id="290" class="Keyword">module</a> <a id="297" href="Data.Char.Properties.html" class="Module">Data.Char.Properties</a> <a id="318" class="Keyword">where</a>
<a id="325" class="Keyword">open</a> <a id="330" class="Keyword">import</a> <a id="337" href="Data.Bool.Base.html" class="Module">Data.Bool.Base</a> <a id="352" class="Keyword">using</a> <a id="358" class="Symbol">(</a><a id="359" href="Agda.Builtin.Bool.html#163" class="Datatype">Bool</a><a id="363" class="Symbol">)</a>
<a id="365" class="Keyword">open</a> <a id="370" class="Keyword">import</a> <a id="377" href="Data.Char.Base.html" class="Module">Data.Char.Base</a>
<a id="392" class="Keyword">import</a> <a id="399" href="Data.Nat.Base.html" class="Module">Data.Nat.Base</a> <a id="413" class="Symbol">as</a> <a id="416" class="Module">ℕ</a>
<a id="418" class="Keyword">import</a> <a id="425" href="Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="445" class="Symbol">as</a> <a id="448" class="Module">ℕₚ</a>
<a id="451" class="Keyword">open</a> <a id="456" class="Keyword">import</a> <a id="463" href="Data.Product.html" class="Module">Data.Product</a> <a id="476" class="Keyword">using</a> <a id="482" class="Symbol">(</a><a id="483" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a><a id="486" class="Symbol">)</a>
<a id="489" class="Keyword">open</a> <a id="494" class="Keyword">import</a> <a id="501" href="Function.Base.html" class="Module">Function.Base</a>
<a id="515" class="Keyword">open</a> <a id="520" class="Keyword">import</a> <a id="527" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="544" class="Keyword">using</a> <a id="550" class="Symbol">(</a><a id="551" href="Relation.Nullary.html#656" class="Function Operator">¬_</a><a id="553" class="Symbol">;</a> <a id="555" href="Relation.Nullary.html#1648" class="InductiveConstructor">yes</a><a id="558" class="Symbol">;</a> <a id="560" href="Relation.Nullary.html#1685" class="InductiveConstructor">no</a><a id="562" class="Symbol">)</a>
<a id="564" class="Keyword">open</a> <a id="569" class="Keyword">import</a> <a id="576" href="Relation.Nullary.Decidable.html" class="Module">Relation.Nullary.Decidable</a> <a id="603" class="Keyword">using</a> <a id="609" class="Symbol">(</a><a id="610" href="Relation.Nullary.Decidable.Core.html#3636" class="Function">map′</a><a id="614" class="Symbol">;</a> <a id="616" href="Relation.Nullary.Decidable.Core.html#1027" class="Function">isYes</a><a id="621" class="Symbol">)</a>
<a id="623" class="Keyword">open</a> <a id="628" class="Keyword">import</a> <a id="635" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="651" class="Keyword">import</a> <a id="658" href="Relation.Binary.Construct.On.html" class="Module">Relation.Binary.Construct.On</a> <a id="687" class="Symbol">as</a> <a id="690" class="Module">On</a>
<a id="693" class="Keyword">import</a> <a id="700" href="Relation.Binary.Construct.Subst.Equality.html" class="Module">Relation.Binary.Construct.Subst.Equality</a> <a id="741" class="Symbol">as</a> <a id="744" class="Module">Subst</a>
<a id="750" class="Keyword">import</a> <a id="757" href="Relation.Binary.Construct.Closure.Reflexive.html" class="Module">Relation.Binary.Construct.Closure.Reflexive</a> <a id="801" class="Symbol">as</a> <a id="804" class="Module">Refl</a>
<a id="809" class="Keyword">import</a> <a id="816" href="Relation.Binary.Construct.Closure.Reflexive.Properties.html" class="Module">Relation.Binary.Construct.Closure.Reflexive.Properties</a> <a id="871" class="Symbol">as</a> <a id="874" class="Module">Reflₚ</a>
<a id="880" class="Keyword">open</a> <a id="885" class="Keyword">import</a> <a id="892" href="Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="930" class="Symbol">as</a> <a id="933" class="Module">PropEq</a>
<a id="942" class="Keyword">using</a> <a id="948" class="Symbol">(</a><a id="949" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a><a id="952" class="Symbol">;</a> <a id="954" href="Relation.Binary.PropositionalEquality.Core.html#830" class="Function Operator">_≢_</a><a id="957" class="Symbol">;</a> <a id="959" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a><a id="963" class="Symbol">;</a> <a id="965" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a><a id="969" class="Symbol">;</a> <a id="971" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a><a id="974" class="Symbol">;</a> <a id="976" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a><a id="981" class="Symbol">;</a> <a id="983" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a><a id="988" class="Symbol">)</a>
<a id="991" class="Comment">------------------------------------------------------------------------</a>
<a id="1064" class="Comment">-- Primitive properties</a>
<a id="1089" class="Keyword">open</a> <a id="1094" class="Keyword">import</a> <a id="1101" href="Agda.Builtin.Char.Properties.html" class="Module">Agda.Builtin.Char.Properties</a>
<a id="1132" class="Keyword">renaming</a> <a id="1141" class="Symbol">(</a> <a id="1143" href="Agda.Builtin.Char.Properties.html#219" class="Primitive">primCharToNatInjective</a> <a id="1166" class="Symbol">to</a> <a id="1169" class="Primitive">toℕ-injective</a><a id="1182" class="Symbol">)</a>
<a id="1186" class="Keyword">public</a>
<a id="1194" class="Comment">------------------------------------------------------------------------</a>
<a id="1267" class="Comment">-- Properties of _≈_</a>
<a id="≈⇒≡"></a><a id="1289" href="Data.Char.Properties.html#1289" class="Function">≈⇒≡</a> <a id="1293" class="Symbol">:</a> <a id="1295" href="Data.Char.Base.html#1260" class="Function Operator">_≈_</a> <a id="1299" href="Relation.Binary.Core.html#1254" class="Function Operator">⇒</a> <a id="1301" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
<a id="1305" href="Data.Char.Properties.html#1289" class="Function">≈⇒≡</a> <a id="1309" class="Symbol">=</a> <a id="1311" href="Data.Char.Properties.html#1169" class="Primitive">toℕ-injective</a> <a id="1325" class="Symbol">_</a> <a id="1327" class="Symbol">_</a>
<a id="≉⇒≢"></a><a id="1330" href="Data.Char.Properties.html#1330" class="Function">≉⇒≢</a> <a id="1334" class="Symbol">:</a> <a id="1336" href="Data.Char.Base.html#1298" class="Function Operator">_≉_</a> <a id="1340" href="Relation.Binary.Core.html#1254" class="Function Operator">⇒</a> <a id="1342" href="Relation.Binary.PropositionalEquality.Core.html#830" class="Function Operator">_≢_</a>
<a id="1346" href="Data.Char.Properties.html#1330" class="Function">≉⇒≢</a> <a id="1350" href="Data.Char.Properties.html#1350" class="Bound">p</a> <a id="1352" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1357" class="Symbol">=</a> <a id="1359" href="Data.Char.Properties.html#1350" class="Bound">p</a> <a id="1361" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
<a id="≈-reflexive"></a><a id="1367" href="Data.Char.Properties.html#1367" class="Function">≈-reflexive</a> <a id="1379" class="Symbol">:</a> <a id="1381" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="1385" href="Relation.Binary.Core.html#1254" class="Function Operator">⇒</a> <a id="1387" href="Data.Char.Base.html#1260" class="Function Operator">_≈_</a>
<a id="1391" href="Data.Char.Properties.html#1367" class="Function">≈-reflexive</a> <a id="1403" class="Symbol">=</a> <a id="1405" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1410" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a>
<a id="1415" class="Comment">------------------------------------------------------------------------</a>
<a id="1488" class="Comment">-- Properties of _≡_</a>
<a id="1510" class="Keyword">infix</a> <a id="1516" class="Number">4</a> <a id="1518" href="Data.Char.Properties.html#1522" class="Function Operator">_≟_</a>
<a id="_≟_"></a><a id="1522" href="Data.Char.Properties.html#1522" class="Function Operator">_≟_</a> <a id="1526" class="Symbol">:</a> <a id="1528" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="1538" class="Symbol">{</a><a id="1539" class="Argument">A</a> <a id="1541" class="Symbol">=</a> <a id="1543" href="Agda.Builtin.Char.html#227" class="Postulate">Char</a><a id="1547" class="Symbol">}</a> <a id="1549" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
<a id="1553" href="Data.Char.Properties.html#1553" class="Bound">x</a> <a id="1555" href="Data.Char.Properties.html#1522" class="Function Operator">≟</a> <a id="1557" href="Data.Char.Properties.html#1557" class="Bound">y</a> <a id="1559" class="Symbol">=</a> <a id="1561" href="Relation.Nullary.Decidable.Core.html#3636" class="Function">map′</a> <a id="1566" href="Data.Char.Properties.html#1289" class="Function">≈⇒≡</a> <a id="1570" href="Data.Char.Properties.html#1367" class="Function">≈-reflexive</a> <a id="1582" class="Symbol">(</a><a id="1583" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a> <a id="1587" href="Data.Char.Properties.html#1553" class="Bound">x</a> <a id="1589" href="Data.Nat.Properties.html#2529" class="Function Operator">ℕₚ.≟</a> <a id="1594" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a> <a id="1598" href="Data.Char.Properties.html#1557" class="Bound">y</a><a id="1599" class="Symbol">)</a>
<a id="setoid"></a><a id="1602" href="Data.Char.Properties.html#1602" class="Function">setoid</a> <a id="1609" class="Symbol">:</a> <a id="1611" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1618" class="Symbol">_</a> <a id="1620" class="Symbol">_</a>
<a id="1622" href="Data.Char.Properties.html#1602" class="Function">setoid</a> <a id="1629" class="Symbol">=</a> <a id="1631" href="Relation.Binary.PropositionalEquality.Properties.html#3972" class="Function">PropEq.setoid</a> <a id="1645" href="Agda.Builtin.Char.html#227" class="Postulate">Char</a>
<a id="decSetoid"></a><a id="1651" href="Data.Char.Properties.html#1651" class="Function">decSetoid</a> <a id="1661" class="Symbol">:</a> <a id="1663" href="Relation.Binary.Bundles.html#1391" class="Record">DecSetoid</a> <a id="1673" class="Symbol">_</a> <a id="1675" class="Symbol">_</a>
<a id="1677" href="Data.Char.Properties.html#1651" class="Function">decSetoid</a> <a id="1687" class="Symbol">=</a> <a id="1689" href="Relation.Binary.PropositionalEquality.Properties.html#4103" class="Function">PropEq.decSetoid</a> <a id="1706" href="Data.Char.Properties.html#1522" class="Function Operator">_≟_</a>
<a id="isDecEquivalence"></a><a id="1711" href="Data.Char.Properties.html#1711" class="Function">isDecEquivalence</a> <a id="1728" class="Symbol">:</a> <a id="1730" href="Relation.Binary.Structures.html#1824" class="Record">IsDecEquivalence</a> <a id="1747" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
<a id="1751" href="Data.Char.Properties.html#1711" class="Function">isDecEquivalence</a> <a id="1768" class="Symbol">=</a> <a id="1770" href="Relation.Binary.PropositionalEquality.Properties.html#3548" class="Function">PropEq.isDecEquivalence</a> <a id="1794" href="Data.Char.Properties.html#1522" class="Function Operator">_≟_</a>
<a id="1799" class="Comment">------------------------------------------------------------------------</a>
<a id="1872" class="Comment">-- Boolean equality test.</a>
<a id="1898" class="Comment">--</a>
<a id="1901" class="Comment">-- Why is the definition _==_ = primCharEquality not used? One reason</a>
<a id="1971" class="Comment">-- is that the present definition can sometimes improve type</a>
<a id="2032" class="Comment">-- inference, at least with the version of Agda that is current at the</a>
<a id="2103" class="Comment">-- time of writing: see unit-test below.</a>
<a id="2145" class="Keyword">infix</a> <a id="2151" class="Number">4</a> <a id="2153" href="Data.Char.Properties.html#2158" class="Function Operator">_==_</a>
<a id="_==_"></a><a id="2158" href="Data.Char.Properties.html#2158" class="Function Operator">_==_</a> <a id="2163" class="Symbol">:</a> <a id="2165" href="Agda.Builtin.Char.html#227" class="Postulate">Char</a> <a id="2170" class="Symbol">→</a> <a id="2172" href="Agda.Builtin.Char.html#227" class="Postulate">Char</a> <a id="2177" class="Symbol">→</a> <a id="2179" href="Agda.Builtin.Bool.html#163" class="Datatype">Bool</a>
<a id="2184" href="Data.Char.Properties.html#2184" class="Bound">c₁</a> <a id="2187" href="Data.Char.Properties.html#2158" class="Function Operator">==</a> <a id="2190" href="Data.Char.Properties.html#2190" class="Bound">c₂</a> <a id="2193" class="Symbol">=</a> <a id="2195" href="Relation.Nullary.Decidable.Core.html#1027" class="Function">isYes</a> <a id="2201" class="Symbol">(</a><a id="2202" href="Data.Char.Properties.html#2184" class="Bound">c₁</a> <a id="2205" href="Data.Char.Properties.html#1522" class="Function Operator">≟</a> <a id="2207" href="Data.Char.Properties.html#2190" class="Bound">c₂</a><a id="2209" class="Symbol">)</a>
<a id="2212" class="Keyword">private</a>
<a id="2223" class="Comment">-- The following unit test does not type-check (at the time of</a>
<a id="2288" class="Comment">-- writing) if _==_ is replaced by primCharEquality.</a>
<a id="2344" class="Keyword">data</a> <a id="P"></a><a id="2349" href="Data.Char.Properties.html#2349" class="Datatype">P</a> <a id="2351" class="Symbol">:</a> <a id="2353" class="Symbol">(</a><a id="2354" href="Agda.Builtin.Char.html#227" class="Postulate">Char</a> <a id="2359" class="Symbol">→</a> <a id="2361" href="Agda.Builtin.Bool.html#163" class="Datatype">Bool</a><a id="2365" class="Symbol">)</a> <a id="2367" class="Symbol">→</a> <a id="2369" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2373" class="Keyword">where</a>
<a id="P.MkP"></a><a id="2383" href="Data.Char.Properties.html#2383" class="InductiveConstructor">MkP</a> <a id="2387" class="Symbol">:</a> <a id="2389" class="Symbol">(</a><a id="2390" href="Data.Char.Properties.html#2390" class="Bound">c</a> <a id="2392" class="Symbol">:</a> <a id="2394" href="Agda.Builtin.Char.html#227" class="Postulate">Char</a><a id="2398" class="Symbol">)</a> <a id="2400" class="Symbol">→</a> <a id="2402" href="Data.Char.Properties.html#2349" class="Datatype">P</a> <a id="2404" class="Symbol">(</a><a id="2405" href="Data.Char.Properties.html#2390" class="Bound">c</a> <a id="2407" href="Data.Char.Properties.html#2158" class="Function Operator">==_</a><a id="2410" class="Symbol">)</a>
<a id="unit-test"></a><a id="2415" href="Data.Char.Properties.html#2415" class="Function">unit-test</a> <a id="2425" class="Symbol">:</a> <a id="2427" href="Data.Char.Properties.html#2349" class="Datatype">P</a> <a id="2429" class="Symbol">(</a><a id="2430" class="String">'x'</a> <a id="2434" href="Data.Char.Properties.html#2158" class="Function Operator">==_</a><a id="2437" class="Symbol">)</a>
<a id="2441" href="Data.Char.Properties.html#2415" class="Function">unit-test</a> <a id="2451" class="Symbol">=</a> <a id="2453" href="Data.Char.Properties.html#2383" class="InductiveConstructor">MkP</a> <a id="2457" class="Symbol">_</a>
<a id="2460" class="Comment">------------------------------------------------------------------------</a>
<a id="2533" class="Comment">-- Properties of _<_</a>
<a id="2555" class="Keyword">infix</a> <a id="2561" class="Number">4</a> <a id="2563" href="Data.Char.Properties.html#2568" class="Function Operator">_<?_</a>
<a id="_<?_"></a><a id="2568" href="Data.Char.Properties.html#2568" class="Function Operator">_<?_</a> <a id="2573" class="Symbol">:</a> <a id="2575" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="2585" href="Data.Char.Base.html#1415" class="Function Operator">_<_</a>
<a id="2589" href="Data.Char.Properties.html#2568" class="Function Operator">_<?_</a> <a id="2594" class="Symbol">=</a> <a id="2596" href="Relation.Binary.Construct.On.html#1784" class="Function">On.decidable</a> <a id="2609" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a> <a id="2613" href="Data.Nat.Base.html#1645" class="Function Operator">ℕ._<_</a> <a id="2619" href="Data.Nat.Properties.html#10078" class="Function Operator">ℕₚ._<?_</a>
<a id="<-cmp"></a><a id="2628" href="Data.Char.Properties.html#2628" class="Function"><-cmp</a> <a id="2634" class="Symbol">:</a> <a id="2636" href="Relation.Binary.Definitions.html#2955" class="Function">Trichotomous</a> <a id="2649" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="2653" href="Data.Char.Base.html#1415" class="Function Operator">_<_</a>
<a id="2657" href="Data.Char.Properties.html#2628" class="Function"><-cmp</a> <a id="2663" href="Data.Char.Properties.html#2663" class="Bound">c</a> <a id="2665" href="Data.Char.Properties.html#2665" class="Bound">d</a> <a id="2667" class="Keyword">with</a> <a id="2672" href="Data.Nat.Properties.html#9763" class="Function">ℕₚ.<-cmp</a> <a id="2681" class="Symbol">(</a><a id="2682" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a> <a id="2686" href="Data.Char.Properties.html#2663" class="Bound">c</a><a id="2687" class="Symbol">)</a> <a id="2689" class="Symbol">(</a><a id="2690" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a> <a id="2694" href="Data.Char.Properties.html#2665" class="Bound">d</a><a id="2695" class="Symbol">)</a>
<a id="2697" class="Symbol">...</a> <a id="2701" class="Symbol">|</a> <a id="2703" href="Relation.Binary.Definitions.html#2778" class="InductiveConstructor">tri<</a> <a id="2708" href="Data.Char.Properties.html#2708" class="Bound">lt</a> <a id="2711" href="Data.Char.Properties.html#2711" class="Bound">¬eq</a> <a id="2715" href="Data.Char.Properties.html#2715" class="Bound">¬gt</a> <a id="2719" class="Symbol">=</a> <a id="2721" href="Relation.Binary.Definitions.html#2778" class="InductiveConstructor">tri<</a> <a id="2726" href="Data.Char.Properties.html#2708" class="Bound">lt</a> <a id="2729" class="Symbol">(</a><a id="2730" href="Data.Char.Properties.html#1330" class="Function">≉⇒≢</a> <a id="2734" href="Data.Char.Properties.html#2711" class="Bound">¬eq</a><a id="2737" class="Symbol">)</a> <a id="2739" href="Data.Char.Properties.html#2715" class="Bound">¬gt</a>
<a id="2743" class="Symbol">...</a> <a id="2747" class="Symbol">|</a> <a id="2749" href="Relation.Binary.Definitions.html#2832" class="InductiveConstructor">tri≈</a> <a id="2754" href="Data.Char.Properties.html#2754" class="Bound">¬lt</a> <a id="2758" href="Data.Char.Properties.html#2758" class="Bound">eq</a> <a id="2761" href="Data.Char.Properties.html#2761" class="Bound">¬gt</a> <a id="2765" class="Symbol">=</a> <a id="2767" href="Relation.Binary.Definitions.html#2832" class="InductiveConstructor">tri≈</a> <a id="2772" href="Data.Char.Properties.html#2754" class="Bound">¬lt</a> <a id="2776" class="Symbol">(</a><a id="2777" href="Data.Char.Properties.html#1289" class="Function">≈⇒≡</a> <a id="2781" href="Data.Char.Properties.html#2758" class="Bound">eq</a><a id="2783" class="Symbol">)</a> <a id="2785" href="Data.Char.Properties.html#2761" class="Bound">¬gt</a>
<a id="2789" class="Symbol">...</a> <a id="2793" class="Symbol">|</a> <a id="2795" href="Relation.Binary.Definitions.html#2886" class="InductiveConstructor">tri></a> <a id="2800" href="Data.Char.Properties.html#2800" class="Bound">¬lt</a> <a id="2804" href="Data.Char.Properties.html#2804" class="Bound">¬eq</a> <a id="2808" href="Data.Char.Properties.html#2808" class="Bound">gt</a> <a id="2811" class="Symbol">=</a> <a id="2813" href="Relation.Binary.Definitions.html#2886" class="InductiveConstructor">tri></a> <a id="2818" href="Data.Char.Properties.html#2800" class="Bound">¬lt</a> <a id="2822" class="Symbol">(</a><a id="2823" href="Data.Char.Properties.html#1330" class="Function">≉⇒≢</a> <a id="2827" href="Data.Char.Properties.html#2804" class="Bound">¬eq</a><a id="2830" class="Symbol">)</a> <a id="2832" href="Data.Char.Properties.html#2808" class="Bound">gt</a>
<a id="<-irrefl"></a><a id="2836" href="Data.Char.Properties.html#2836" class="Function"><-irrefl</a> <a id="2845" class="Symbol">:</a> <a id="2847" href="Relation.Binary.Definitions.html#2241" class="Function">Irreflexive</a> <a id="2859" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="2863" href="Data.Char.Base.html#1415" class="Function Operator">_<_</a>
<a id="2867" href="Data.Char.Properties.html#2836" class="Function"><-irrefl</a> <a id="2876" class="Symbol">=</a> <a id="2878" href="Data.Nat.Properties.html#9065" class="Function">ℕₚ.<-irrefl</a> <a id="2890" href="Function.Base.html#3706" class="Function Operator">∘′</a> <a id="2893" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="2898" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a>
<a id="<-trans"></a><a id="2903" href="Data.Char.Properties.html#2903" class="Function"><-trans</a> <a id="2911" class="Symbol">:</a> <a id="2913" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="2924" href="Data.Char.Base.html#1415" class="Function Operator">_<_</a>
<a id="2928" href="Data.Char.Properties.html#2903" class="Function"><-trans</a> <a id="2936" class="Symbol">{</a><a id="2937" href="Data.Char.Properties.html#2937" class="Bound">c</a><a id="2938" class="Symbol">}</a> <a id="2940" class="Symbol">{</a><a id="2941" href="Data.Char.Properties.html#2941" class="Bound">d</a><a id="2942" class="Symbol">}</a> <a id="2944" class="Symbol">{</a><a id="2945" href="Data.Char.Properties.html#2945" class="Bound">e</a><a id="2946" class="Symbol">}</a> <a id="2948" class="Symbol">=</a> <a id="2950" href="Relation.Binary.Construct.On.html#1147" class="Function">On.transitive</a> <a id="2964" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a> <a id="2968" href="Data.Nat.Base.html#1645" class="Function Operator">ℕ._<_</a> <a id="2974" href="Data.Nat.Properties.html#9210" class="Function">ℕₚ.<-trans</a> <a id="2985" class="Symbol">{</a><a id="2986" href="Data.Char.Properties.html#2937" class="Bound">c</a><a id="2987" class="Symbol">}</a> <a id="2989" class="Symbol">{</a><a id="2990" href="Data.Char.Properties.html#2941" class="Bound">d</a><a id="2991" class="Symbol">}</a> <a id="2993" class="Symbol">{</a><a id="2994" href="Data.Char.Properties.html#2945" class="Bound">e</a><a id="2995" class="Symbol">}</a>
<a id="<-asym"></a><a id="2998" href="Data.Char.Properties.html#2998" class="Function"><-asym</a> <a id="3005" class="Symbol">:</a> <a id="3007" href="Relation.Binary.Definitions.html#2353" class="Function">Asymmetric</a> <a id="3018" href="Data.Char.Base.html#1415" class="Function Operator">_<_</a>
<a id="3022" href="Data.Char.Properties.html#2998" class="Function"><-asym</a> <a id="3029" class="Symbol">{</a><a id="3030" href="Data.Char.Properties.html#3030" class="Bound">c</a><a id="3031" class="Symbol">}</a> <a id="3033" class="Symbol">{</a><a id="3034" href="Data.Char.Properties.html#3034" class="Bound">d</a><a id="3035" class="Symbol">}</a> <a id="3037" class="Symbol">=</a> <a id="3039" href="Relation.Binary.Construct.On.html#1402" class="Function">On.asymmetric</a> <a id="3053" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a> <a id="3057" href="Data.Nat.Base.html#1645" class="Function Operator">ℕ._<_</a> <a id="3063" href="Data.Nat.Properties.html#9141" class="Function">ℕₚ.<-asym</a> <a id="3073" class="Symbol">{</a><a id="3074" href="Data.Char.Properties.html#3030" class="Bound">c</a><a id="3075" class="Symbol">}</a> <a id="3077" class="Symbol">{</a><a id="3078" href="Data.Char.Properties.html#3034" class="Bound">d</a><a id="3079" class="Symbol">}</a>
<a id="<-isStrictPartialOrder"></a><a id="3082" href="Data.Char.Properties.html#3082" class="Function"><-isStrictPartialOrder</a> <a id="3105" class="Symbol">:</a> <a id="3107" href="Relation.Binary.Structures.html#3950" class="Record">IsStrictPartialOrder</a> <a id="3128" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="3132" href="Data.Char.Base.html#1415" class="Function Operator">_<_</a>
<a id="3136" href="Data.Char.Properties.html#3082" class="Function"><-isStrictPartialOrder</a> <a id="3159" class="Symbol">=</a> <a id="3161" class="Keyword">record</a>
<a id="3170" class="Symbol">{</a> <a id="3172" href="Relation.Binary.Structures.html#4025" class="Field">isEquivalence</a> <a id="3186" class="Symbol">=</a> <a id="3188" href="Relation.Binary.PropositionalEquality.Properties.html#3427" class="Function">PropEq.isEquivalence</a>
<a id="3211" class="Symbol">;</a> <a id="3213" href="Relation.Binary.Structures.html#4059" class="Field">irrefl</a> <a id="3227" class="Symbol">=</a> <a id="3229" href="Data.Char.Properties.html#2836" class="Function"><-irrefl</a>
<a id="3240" class="Symbol">;</a> <a id="3242" href="Relation.Binary.Structures.html#4099" class="Field">trans</a> <a id="3256" class="Symbol">=</a> <a id="3258" class="Symbol">λ</a> <a id="3260" class="Symbol">{</a><a id="3261" href="Data.Char.Properties.html#3261" class="Bound">a</a><a id="3262" class="Symbol">}</a> <a id="3264" class="Symbol">{</a><a id="3265" href="Data.Char.Properties.html#3265" class="Bound">b</a><a id="3266" class="Symbol">}</a> <a id="3268" class="Symbol">{</a><a id="3269" href="Data.Char.Properties.html#3269" class="Bound">c</a><a id="3270" class="Symbol">}</a> <a id="3272" class="Symbol">→</a> <a id="3274" href="Data.Char.Properties.html#2903" class="Function"><-trans</a> <a id="3282" class="Symbol">{</a><a id="3283" href="Data.Char.Properties.html#3261" class="Bound">a</a><a id="3284" class="Symbol">}</a> <a id="3286" class="Symbol">{</a><a id="3287" href="Data.Char.Properties.html#3265" class="Bound">b</a><a id="3288" class="Symbol">}</a> <a id="3290" class="Symbol">{</a><a id="3291" href="Data.Char.Properties.html#3269" class="Bound">c</a><a id="3292" class="Symbol">}</a>
<a id="3296" class="Symbol">;</a> <a id="3298" href="Relation.Binary.Structures.html#4134" class="Field"><-resp-≈</a> <a id="3312" class="Symbol">=</a> <a id="3314" class="Symbol">(λ</a> <a id="3317" class="Symbol">{</a><a id="3318" href="Data.Char.Properties.html#3318" class="Bound">c</a><a id="3319" class="Symbol">}</a> <a id="3321" class="Symbol">→</a> <a id="3323" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">PropEq.subst</a> <a id="3336" class="Symbol">(</a><a id="3337" href="Data.Char.Properties.html#3318" class="Bound">c</a> <a id="3339" href="Data.Char.Base.html#1415" class="Function Operator"><_</a><a id="3341" class="Symbol">))</a>
<a id="3362" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3364" class="Symbol">(λ</a> <a id="3367" class="Symbol">{</a><a id="3368" href="Data.Char.Properties.html#3368" class="Bound">c</a><a id="3369" class="Symbol">}</a> <a id="3371" class="Symbol">→</a> <a id="3373" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">PropEq.subst</a> <a id="3386" class="Symbol">(</a><a id="3387" href="Data.Char.Base.html#1415" class="Function Operator">_<</a> <a id="3390" href="Data.Char.Properties.html#3368" class="Bound">c</a><a id="3391" class="Symbol">))</a>
<a id="3396" class="Symbol">}</a>
<a id="<-isStrictTotalOrder"></a><a id="3399" href="Data.Char.Properties.html#3399" class="Function"><-isStrictTotalOrder</a> <a id="3420" class="Symbol">:</a> <a id="3422" href="Relation.Binary.Structures.html#6539" class="Record">IsStrictTotalOrder</a> <a id="3441" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="3445" href="Data.Char.Base.html#1415" class="Function Operator">_<_</a>
<a id="3449" href="Data.Char.Properties.html#3399" class="Function"><-isStrictTotalOrder</a> <a id="3470" class="Symbol">=</a> <a id="3472" class="Keyword">record</a>
<a id="3481" class="Symbol">{</a> <a id="3483" href="Relation.Binary.Structures.html#6612" class="Field">isEquivalence</a> <a id="3497" class="Symbol">=</a> <a id="3499" href="Relation.Binary.PropositionalEquality.Properties.html#3427" class="Function">PropEq.isEquivalence</a>
<a id="3522" class="Symbol">;</a> <a id="3524" href="Relation.Binary.Structures.html#6646" class="Field">trans</a> <a id="3538" class="Symbol">=</a> <a id="3540" class="Symbol">λ</a> <a id="3542" class="Symbol">{</a><a id="3543" href="Data.Char.Properties.html#3543" class="Bound">a</a><a id="3544" class="Symbol">}</a> <a id="3546" class="Symbol">{</a><a id="3547" href="Data.Char.Properties.html#3547" class="Bound">b</a><a id="3548" class="Symbol">}</a> <a id="3550" class="Symbol">{</a><a id="3551" href="Data.Char.Properties.html#3551" class="Bound">c</a><a id="3552" class="Symbol">}</a> <a id="3554" class="Symbol">→</a> <a id="3556" href="Data.Char.Properties.html#2903" class="Function"><-trans</a> <a id="3564" class="Symbol">{</a><a id="3565" href="Data.Char.Properties.html#3543" class="Bound">a</a><a id="3566" class="Symbol">}</a> <a id="3568" class="Symbol">{</a><a id="3569" href="Data.Char.Properties.html#3547" class="Bound">b</a><a id="3570" class="Symbol">}</a> <a id="3572" class="Symbol">{</a><a id="3573" href="Data.Char.Properties.html#3551" class="Bound">c</a><a id="3574" class="Symbol">}</a>
<a id="3578" class="Symbol">;</a> <a id="3580" href="Relation.Binary.Structures.html#6681" class="Field">compare</a> <a id="3594" class="Symbol">=</a> <a id="3596" href="Data.Char.Properties.html#2628" class="Function"><-cmp</a>
<a id="3604" class="Symbol">}</a>
<a id="<-strictPartialOrder"></a><a id="3607" href="Data.Char.Properties.html#3607" class="Function"><-strictPartialOrder</a> <a id="3628" class="Symbol">:</a> <a id="3630" href="Relation.Binary.Bundles.html#4108" class="Record">StrictPartialOrder</a> <a id="3649" class="Symbol">_</a> <a id="3651" class="Symbol">_</a> <a id="3653" class="Symbol">_</a>
<a id="3655" href="Data.Char.Properties.html#3607" class="Function"><-strictPartialOrder</a> <a id="3676" class="Symbol">=</a> <a id="3678" class="Keyword">record</a>
<a id="3687" class="Symbol">{</a> <a id="3689" href="Relation.Binary.Bundles.html#4314" class="Field">isStrictPartialOrder</a> <a id="3710" class="Symbol">=</a> <a id="3712" href="Data.Char.Properties.html#3082" class="Function"><-isStrictPartialOrder</a>
<a id="3737" class="Symbol">}</a>
<a id="<-strictTotalOrder"></a><a id="3740" href="Data.Char.Properties.html#3740" class="Function"><-strictTotalOrder</a> <a id="3759" class="Symbol">:</a> <a id="3761" href="Relation.Binary.Bundles.html#6928" class="Record">StrictTotalOrder</a> <a id="3778" class="Symbol">_</a> <a id="3780" class="Symbol">_</a> <a id="3782" class="Symbol">_</a>
<a id="3784" href="Data.Char.Properties.html#3740" class="Function"><-strictTotalOrder</a> <a id="3803" class="Symbol">=</a> <a id="3805" class="Keyword">record</a>
<a id="3814" class="Symbol">{</a> <a id="3816" href="Relation.Binary.Bundles.html#7126" class="Field">isStrictTotalOrder</a> <a id="3835" class="Symbol">=</a> <a id="3837" href="Data.Char.Properties.html#3399" class="Function"><-isStrictTotalOrder</a>
<a id="3860" class="Symbol">}</a>
<a id="3863" class="Comment">------------------------------------------------------------------------</a>
<a id="3936" class="Comment">-- Properties of _≤_</a>
<a id="3958" class="Keyword">infix</a> <a id="3964" class="Number">4</a> <a id="3966" href="Data.Char.Properties.html#3971" class="Function Operator">_≤?_</a>
<a id="_≤?_"></a><a id="3971" href="Data.Char.Properties.html#3971" class="Function Operator">_≤?_</a> <a id="3976" class="Symbol">:</a> <a id="3978" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="3988" href="Data.Char.Base.html#1467" class="Function Operator">_≤_</a>
<a id="3992" href="Data.Char.Properties.html#3971" class="Function Operator">_≤?_</a> <a id="3997" class="Symbol">=</a> <a id="3999" href="Relation.Binary.Construct.Closure.Reflexive.Properties.html#2501" class="Function">Reflₚ.decidable</a> <a id="4015" href="Data.Char.Properties.html#2628" class="Function"><-cmp</a>
<a id="≤-reflexive"></a><a id="4022" href="Data.Char.Properties.html#4022" class="Function">≤-reflexive</a> <a id="4034" class="Symbol">:</a> <a id="4036" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="4040" href="Relation.Binary.Core.html#1254" class="Function Operator">⇒</a> <a id="4042" href="Data.Char.Base.html#1467" class="Function Operator">_≤_</a>
<a id="4046" href="Data.Char.Properties.html#4022" class="Function">≤-reflexive</a> <a id="4058" class="Symbol">=</a> <a id="4060" href="Relation.Binary.Construct.Closure.Reflexive.html#1459" class="Function">Refl.reflexive</a>
<a id="≤-trans"></a><a id="4076" href="Data.Char.Properties.html#4076" class="Function">≤-trans</a> <a id="4084" class="Symbol">:</a> <a id="4086" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="4097" href="Data.Char.Base.html#1467" class="Function Operator">_≤_</a>
<a id="4101" href="Data.Char.Properties.html#4076" class="Function">≤-trans</a> <a id="4109" class="Symbol">=</a> <a id="4111" href="Relation.Binary.Construct.Closure.Reflexive.Properties.html#1699" class="Function">Reflₚ.trans</a> <a id="4123" class="Symbol">(λ</a> <a id="4126" class="Symbol">{</a><a id="4127" href="Data.Char.Properties.html#4127" class="Bound">a</a><a id="4128" class="Symbol">}</a> <a id="4130" class="Symbol">{</a><a id="4131" href="Data.Char.Properties.html#4131" class="Bound">b</a><a id="4132" class="Symbol">}</a> <a id="4134" class="Symbol">{</a><a id="4135" href="Data.Char.Properties.html#4135" class="Bound">c</a><a id="4136" class="Symbol">}</a> <a id="4138" class="Symbol">→</a> <a id="4140" href="Data.Char.Properties.html#2903" class="Function"><-trans</a> <a id="4148" class="Symbol">{</a><a id="4149" href="Data.Char.Properties.html#4127" class="Bound">a</a><a id="4150" class="Symbol">}</a> <a id="4152" class="Symbol">{</a><a id="4153" href="Data.Char.Properties.html#4131" class="Bound">b</a><a id="4154" class="Symbol">}</a> <a id="4156" class="Symbol">{</a><a id="4157" href="Data.Char.Properties.html#4135" class="Bound">c</a><a id="4158" class="Symbol">})</a>
<a id="≤-antisym"></a><a id="4162" href="Data.Char.Properties.html#4162" class="Function">≤-antisym</a> <a id="4172" class="Symbol">:</a> <a id="4174" href="Relation.Binary.Definitions.html#2082" class="Function">Antisymmetric</a> <a id="4188" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="4192" href="Data.Char.Base.html#1467" class="Function Operator">_≤_</a>
<a id="4196" href="Data.Char.Properties.html#4162" class="Function">≤-antisym</a> <a id="4206" class="Symbol">=</a> <a id="4208" href="Relation.Binary.Construct.Closure.Reflexive.Properties.html#1925" class="Function">Reflₚ.antisym</a> <a id="4222" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="4226" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="4231" href="Data.Nat.Properties.html#9141" class="Function">ℕₚ.<-asym</a>
<a id="≤-isPreorder"></a><a id="4242" href="Data.Char.Properties.html#4242" class="Function">≤-isPreorder</a> <a id="4255" class="Symbol">:</a> <a id="4257" href="Relation.Binary.Structures.html#2163" class="Record">IsPreorder</a> <a id="4268" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="4272" href="Data.Char.Base.html#1467" class="Function Operator">_≤_</a>
<a id="4276" href="Data.Char.Properties.html#4242" class="Function">≤-isPreorder</a> <a id="4289" class="Symbol">=</a> <a id="4291" class="Keyword">record</a>
<a id="4300" class="Symbol">{</a> <a id="4302" href="Relation.Binary.Structures.html#2228" class="Field">isEquivalence</a> <a id="4316" class="Symbol">=</a> <a id="4318" href="Relation.Binary.PropositionalEquality.Properties.html#3427" class="Function">PropEq.isEquivalence</a>
<a id="4341" class="Symbol">;</a> <a id="4343" href="Relation.Binary.Structures.html#2331" class="Field">reflexive</a> <a id="4357" class="Symbol">=</a> <a id="4359" href="Data.Char.Properties.html#4022" class="Function">≤-reflexive</a>
<a id="4373" class="Symbol">;</a> <a id="4375" href="Relation.Binary.Structures.html#2361" class="Field">trans</a> <a id="4389" class="Symbol">=</a> <a id="4391" href="Data.Char.Properties.html#4076" class="Function">≤-trans</a>
<a id="4401" class="Symbol">}</a>
<a id="≤-isPartialOrder"></a><a id="4404" href="Data.Char.Properties.html#4404" class="Function">≤-isPartialOrder</a> <a id="4421" class="Symbol">:</a> <a id="4423" href="Relation.Binary.Structures.html#3174" class="Record">IsPartialOrder</a> <a id="4438" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="4442" href="Data.Char.Base.html#1467" class="Function Operator">_≤_</a>
<a id="4446" href="Data.Char.Properties.html#4404" class="Function">≤-isPartialOrder</a> <a id="4463" class="Symbol">=</a> <a id="4465" class="Keyword">record</a>
<a id="4474" class="Symbol">{</a> <a id="4476" href="Relation.Binary.Structures.html#3243" class="Field">isPreorder</a> <a id="4487" class="Symbol">=</a> <a id="4489" href="Data.Char.Properties.html#4242" class="Function">≤-isPreorder</a>
<a id="4504" class="Symbol">;</a> <a id="4506" href="Relation.Binary.Structures.html#3275" class="Field">antisym</a> <a id="4517" class="Symbol">=</a> <a id="4519" href="Data.Char.Properties.html#4162" class="Function">≤-antisym</a>
<a id="4531" class="Symbol">}</a>
<a id="≤-isDecPartialOrder"></a><a id="4534" href="Data.Char.Properties.html#4534" class="Function">≤-isDecPartialOrder</a> <a id="4554" class="Symbol">:</a> <a id="4556" href="Relation.Binary.Structures.html#3461" class="Record">IsDecPartialOrder</a> <a id="4574" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="4578" href="Data.Char.Base.html#1467" class="Function Operator">_≤_</a>
<a id="4582" href="Data.Char.Properties.html#4534" class="Function">≤-isDecPartialOrder</a> <a id="4602" class="Symbol">=</a> <a id="4604" class="Keyword">record</a>
<a id="4613" class="Symbol">{</a> <a id="4615" href="Relation.Binary.Structures.html#3552" class="Field">isPartialOrder</a> <a id="4630" class="Symbol">=</a> <a id="4632" href="Data.Char.Properties.html#4404" class="Function">≤-isPartialOrder</a>
<a id="4651" class="Symbol">;</a> <a id="4653" href="Relation.Binary.Structures.html#3592" class="Field Operator">_≟_</a> <a id="4668" class="Symbol">=</a> <a id="4670" href="Data.Char.Properties.html#1522" class="Function Operator">_≟_</a>
<a id="4676" class="Symbol">;</a> <a id="4678" href="Relation.Binary.Structures.html#3627" class="Field Operator">_≤?_</a> <a id="4693" class="Symbol">=</a> <a id="4695" href="Data.Char.Properties.html#3971" class="Function Operator">_≤?_</a>
<a id="4702" class="Symbol">}</a>
<a id="≤-preorder"></a><a id="4705" href="Data.Char.Properties.html#4705" class="Function">≤-preorder</a> <a id="4716" class="Symbol">:</a> <a id="4718" href="Relation.Binary.Bundles.html#1920" class="Record">Preorder</a> <a id="4727" class="Symbol">_</a> <a id="4729" class="Symbol">_</a> <a id="4731" class="Symbol">_</a>
<a id="4733" href="Data.Char.Properties.html#4705" class="Function">≤-preorder</a> <a id="4744" class="Symbol">=</a> <a id="4746" class="Keyword">record</a> <a id="4753" class="Symbol">{</a> <a id="4755" href="Relation.Binary.Bundles.html#2133" class="Field">isPreorder</a> <a id="4766" class="Symbol">=</a> <a id="4768" href="Data.Char.Properties.html#4242" class="Function">≤-isPreorder</a> <a id="4781" class="Symbol">}</a>
<a id="≤-poset"></a><a id="4784" href="Data.Char.Properties.html#4784" class="Function">≤-poset</a> <a id="4792" class="Symbol">:</a> <a id="4794" href="Relation.Binary.Bundles.html#3028" class="Record">Poset</a> <a id="4800" class="Symbol">_</a> <a id="4802" class="Symbol">_</a> <a id="4804" class="Symbol">_</a>
<a id="4806" href="Data.Char.Properties.html#4784" class="Function">≤-poset</a> <a id="4814" class="Symbol">=</a> <a id="4816" class="Keyword">record</a> <a id="4823" class="Symbol">{</a> <a id="4825" href="Relation.Binary.Bundles.html#3203" class="Field">isPartialOrder</a> <a id="4840" class="Symbol">=</a> <a id="4842" href="Data.Char.Properties.html#4404" class="Function">≤-isPartialOrder</a> <a id="4859" class="Symbol">}</a>
<a id="≤-decPoset"></a><a id="4862" href="Data.Char.Properties.html#4862" class="Function">≤-decPoset</a> <a id="4873" class="Symbol">:</a> <a id="4875" href="Relation.Binary.Bundles.html#3462" class="Record">DecPoset</a> <a id="4884" class="Symbol">_</a> <a id="4886" class="Symbol">_</a> <a id="4888" class="Symbol">_</a>
<a id="4890" href="Data.Char.Properties.html#4862" class="Function">≤-decPoset</a> <a id="4901" class="Symbol">=</a> <a id="4903" class="Keyword">record</a> <a id="4910" class="Symbol">{</a> <a id="4912" href="Relation.Binary.Bundles.html#3649" class="Field">isDecPartialOrder</a> <a id="4930" class="Symbol">=</a> <a id="4932" href="Data.Char.Properties.html#4534" class="Function">≤-isDecPartialOrder</a> <a id="4952" class="Symbol">}</a>
<a id="4955" class="Comment">------------------------------------------------------------------------</a>
<a id="5028" class="Comment">-- DEPRECATED NAMES</a>
<a id="5048" class="Comment">------------------------------------------------------------------------</a>
<a id="5121" class="Comment">-- Please use the new names as continuing support for the old names is</a>
<a id="5192" class="Comment">-- not guaranteed.</a>
<a id="5212" class="Comment">-- Version 1.1</a>
<a id="toNat-injective"></a><a id="5228" href="Data.Char.Properties.html#5228" class="Function">toNat-injective</a> <a id="5244" class="Symbol">=</a> <a id="5246" href="Data.Char.Properties.html#1169" class="Primitive">toℕ-injective</a>
<a id="5260" class="Symbol">{-#</a> <a id="5264" class="Keyword">WARNING_ON_USAGE</a> <a id="5281" class="Pragma">toℕ-injective</a>
<a id="5295" class="String">"Warning: toNat-injective was deprecated in v1.1.
Please use toℕ-injective instead."</a>
<a id="5380" class="Symbol">#-}</a>
<a id="strictTotalOrder"></a><a id="5385" href="Data.Char.Properties.html#5385" class="Function">strictTotalOrder</a> <a id="5402" class="Symbol">=</a> <a id="5404" href="Relation.Binary.Construct.On.html#7045" class="Function">On.strictTotalOrder</a> <a id="5424" href="Data.Nat.Properties.html#10895" class="Function">ℕₚ.<-strictTotalOrder</a> <a id="5446" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a>
<a id="5450" class="Symbol">{-#</a> <a id="5454" class="Keyword">WARNING_ON_USAGE</a> <a id="5471" class="Pragma">strictTotalOrder</a>
<a id="5488" class="String">"Warning: strictTotalOrder was deprecated in v1.1.
Please use <-strictTotalOrder-≈ instead."</a>
<a id="5581" class="Symbol">#-}</a>
<a id="5586" class="Comment">-- Version 1.5</a>
<a id="5602" class="Keyword">infix</a> <a id="5608" class="Number">4</a> <a id="5610" href="Data.Char.Properties.html#5615" class="Function Operator">_≈?_</a>
<a id="_≈?_"></a><a id="5615" href="Data.Char.Properties.html#5615" class="Function Operator">_≈?_</a> <a id="5620" class="Symbol">:</a> <a id="5622" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="5632" href="Data.Char.Base.html#1260" class="Function Operator">_≈_</a>
<a id="5636" href="Data.Char.Properties.html#5636" class="Bound">x</a> <a id="5638" href="Data.Char.Properties.html#5615" class="Function Operator">≈?</a> <a id="5641" href="Data.Char.Properties.html#5641" class="Bound">y</a> <a id="5643" class="Symbol">=</a> <a id="5645" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a> <a id="5649" href="Data.Char.Properties.html#5636" class="Bound">x</a> <a id="5651" href="Data.Nat.Properties.html#2529" class="Function Operator">ℕₚ.≟</a> <a id="5656" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a> <a id="5660" href="Data.Char.Properties.html#5641" class="Bound">y</a>
<a id="5662" class="Symbol">{-#</a> <a id="5666" class="Keyword">WARNING_ON_USAGE</a> <a id="5683" class="Pragma">_≈?_</a>
<a id="5688" class="String">"Warning: _≈?_ was deprecated in v1.5.
Please use _≟_ instead."</a>
<a id="5752" class="Symbol">#-}</a>
<a id="≈-refl"></a><a id="5757" href="Data.Char.Properties.html#5757" class="Function">≈-refl</a> <a id="5764" class="Symbol">:</a> <a id="5766" href="Relation.Binary.Definitions.html#1339" class="Function">Reflexive</a> <a id="5776" href="Data.Char.Base.html#1260" class="Function Operator">_≈_</a>
<a id="5780" href="Data.Char.Properties.html#5757" class="Function">≈-refl</a> <a id="5787" class="Symbol">=</a> <a id="5789" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
<a id="5794" class="Symbol">{-#</a> <a id="5798" class="Keyword">WARNING_ON_USAGE</a> <a id="5815" class="Pragma">≈-refl</a>
<a id="5822" class="String">"Warning: ≈-refl was deprecated in v1.5.
Please use Propositional Equality's refl instead."</a>
<a id="5914" class="Symbol">#-}</a>
<a id="≈-sym"></a><a id="5919" href="Data.Char.Properties.html#5919" class="Function">≈-sym</a> <a id="5925" class="Symbol">:</a> <a id="5927" href="Relation.Binary.Definitions.html#1498" class="Function">Symmetric</a> <a id="5937" href="Data.Char.Base.html#1260" class="Function Operator">_≈_</a>
<a id="5941" href="Data.Char.Properties.html#5919" class="Function">≈-sym</a> <a id="5947" class="Symbol">=</a> <a id="5949" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a>
<a id="5953" class="Symbol">{-#</a> <a id="5957" class="Keyword">WARNING_ON_USAGE</a> <a id="5974" class="Pragma">≈-sym</a>
<a id="5980" class="String">"Warning: ≈-sym was deprecated in v1.5.
Please use Propositional Equality's sym instead."</a>
<a id="6070" class="Symbol">#-}</a>
<a id="≈-trans"></a><a id="6075" href="Data.Char.Properties.html#6075" class="Function">≈-trans</a> <a id="6083" class="Symbol">:</a> <a id="6085" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="6096" href="Data.Char.Base.html#1260" class="Function Operator">_≈_</a>
<a id="6100" href="Data.Char.Properties.html#6075" class="Function">≈-trans</a> <a id="6108" class="Symbol">=</a> <a id="6110" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a>
<a id="6116" class="Symbol">{-#</a> <a id="6120" class="Keyword">WARNING_ON_USAGE</a> <a id="6137" class="Pragma">≈-trans</a>
<a id="6145" class="String">"Warning: ≈-trans was deprecated in v1.5.
Please use Propositional Equality's trans instead."</a>
<a id="6239" class="Symbol">#-}</a>
<a id="≈-subst"></a><a id="6244" href="Data.Char.Properties.html#6244" class="Function">≈-subst</a> <a id="6252" class="Symbol">:</a> <a id="6254" class="Symbol">∀</a> <a id="6256" class="Symbol">{</a><a id="6257" href="Data.Char.Properties.html#6257" class="Bound">ℓ</a><a id="6258" class="Symbol">}</a> <a id="6260" class="Symbol">→</a> <a id="6262" href="Relation.Binary.Definitions.html#4369" class="Function">Substitutive</a> <a id="6275" href="Data.Char.Base.html#1260" class="Function Operator">_≈_</a> <a id="6279" href="Data.Char.Properties.html#6257" class="Bound">ℓ</a>
<a id="6281" href="Data.Char.Properties.html#6244" class="Function">≈-subst</a> <a id="6289" href="Data.Char.Properties.html#6289" class="Bound">P</a> <a id="6291" href="Data.Char.Properties.html#6291" class="Bound">x≈y</a> <a id="6295" href="Data.Char.Properties.html#6295" class="Bound">p</a> <a id="6297" class="Symbol">=</a> <a id="6299" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="6305" href="Data.Char.Properties.html#6289" class="Bound">P</a> <a id="6307" class="Symbol">(</a><a id="6308" href="Data.Char.Properties.html#1289" class="Function">≈⇒≡</a> <a id="6312" href="Data.Char.Properties.html#6291" class="Bound">x≈y</a><a id="6315" class="Symbol">)</a> <a id="6317" href="Data.Char.Properties.html#6295" class="Bound">p</a>
<a id="6319" class="Symbol">{-#</a> <a id="6323" class="Keyword">WARNING_ON_USAGE</a> <a id="6340" class="Pragma">≈-subst</a>
<a id="6348" class="String">"Warning: ≈-subst was deprecated in v1.5.
Please use Propositional Equality's subst instead."</a>
<a id="6442" class="Symbol">#-}</a>
<a id="≈-isEquivalence"></a><a id="6447" href="Data.Char.Properties.html#6447" class="Function">≈-isEquivalence</a> <a id="6463" class="Symbol">:</a> <a id="6465" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a> <a id="6479" href="Data.Char.Base.html#1260" class="Function Operator">_≈_</a>
<a id="6483" href="Data.Char.Properties.html#6447" class="Function">≈-isEquivalence</a> <a id="6499" class="Symbol">=</a> <a id="6501" class="Keyword">record</a>
<a id="6510" class="Symbol">{</a> <a id="6512" href="Relation.Binary.Structures.html#1568" class="Field">refl</a> <a id="6518" class="Symbol">=</a> <a id="6520" class="Symbol">λ</a> <a id="6522" class="Symbol">{</a><a id="6523" href="Data.Char.Properties.html#6523" class="Bound">i</a><a id="6524" class="Symbol">}</a> <a id="6526" class="Symbol">→</a> <a id="6528" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
<a id="6535" class="Symbol">;</a> <a id="6537" href="Relation.Binary.Structures.html#1594" class="Field">sym</a> <a id="6543" class="Symbol">=</a> <a id="6545" class="Symbol">λ</a> <a id="6547" class="Symbol">{</a><a id="6548" href="Data.Char.Properties.html#6548" class="Bound">i</a> <a id="6550" href="Data.Char.Properties.html#6550" class="Bound">j</a><a id="6551" class="Symbol">}</a> <a id="6553" class="Symbol">→</a> <a id="6555" href="Data.Char.Properties.html#5919" class="Function">≈-sym</a> <a id="6561" class="Symbol">{</a><a id="6562" href="Data.Char.Properties.html#6548" class="Bound">i</a><a id="6563" class="Symbol">}</a> <a id="6565" class="Symbol">{</a><a id="6566" href="Data.Char.Properties.html#6550" class="Bound">j</a><a id="6567" class="Symbol">}</a>
<a id="6571" class="Symbol">;</a> <a id="6573" href="Relation.Binary.Structures.html#1620" class="Field">trans</a> <a id="6579" class="Symbol">=</a> <a id="6581" class="Symbol">λ</a> <a id="6583" class="Symbol">{</a><a id="6584" href="Data.Char.Properties.html#6584" class="Bound">i</a> <a id="6586" href="Data.Char.Properties.html#6586" class="Bound">j</a> <a id="6588" href="Data.Char.Properties.html#6588" class="Bound">k</a><a id="6589" class="Symbol">}</a> <a id="6591" class="Symbol">→</a> <a id="6593" href="Data.Char.Properties.html#6075" class="Function">≈-trans</a> <a id="6601" class="Symbol">{</a><a id="6602" href="Data.Char.Properties.html#6584" class="Bound">i</a><a id="6603" class="Symbol">}</a> <a id="6605" class="Symbol">{</a><a id="6606" href="Data.Char.Properties.html#6586" class="Bound">j</a><a id="6607" class="Symbol">}</a> <a id="6609" class="Symbol">{</a><a id="6610" href="Data.Char.Properties.html#6588" class="Bound">k</a><a id="6611" class="Symbol">}</a>
<a id="6615" class="Symbol">}</a>
<a id="6617" class="Symbol">{-#</a> <a id="6621" class="Keyword">WARNING_ON_USAGE</a> <a id="6638" class="Pragma">≈-isEquivalence</a>
<a id="6654" class="String">"Warning: ≈-isEquivalence was deprecated in v1.5.
Please use Propositional Equality's isEquivalence instead."</a>
<a id="6764" class="Symbol">#-}</a>
<a id="≈-setoid"></a><a id="6769" href="Data.Char.Properties.html#6769" class="Function">≈-setoid</a> <a id="6778" class="Symbol">:</a> <a id="6780" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="6787" class="Symbol">_</a> <a id="6789" class="Symbol">_</a>
<a id="6791" href="Data.Char.Properties.html#6769" class="Function">≈-setoid</a> <a id="6800" class="Symbol">=</a> <a id="6802" class="Keyword">record</a>
<a id="6811" class="Symbol">{</a> <a id="6813" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="6827" class="Symbol">=</a> <a id="6829" href="Data.Char.Properties.html#6447" class="Function">≈-isEquivalence</a>
<a id="6847" class="Symbol">}</a>
<a id="6849" class="Symbol">{-#</a> <a id="6853" class="Keyword">WARNING_ON_USAGE</a> <a id="6870" class="Pragma">≈-setoid</a>
<a id="6879" class="String">"Warning: ≈-setoid was deprecated in v1.5.
Please use Propositional Equality's setoid instead."</a>
<a id="6975" class="Symbol">#-}</a>
<a id="≈-isDecEquivalence"></a><a id="6980" href="Data.Char.Properties.html#6980" class="Function">≈-isDecEquivalence</a> <a id="6999" class="Symbol">:</a> <a id="7001" href="Relation.Binary.Structures.html#1824" class="Record">IsDecEquivalence</a> <a id="7018" href="Data.Char.Base.html#1260" class="Function Operator">_≈_</a>
<a id="7022" href="Data.Char.Properties.html#6980" class="Function">≈-isDecEquivalence</a> <a id="7041" class="Symbol">=</a> <a id="7043" class="Keyword">record</a>
<a id="7052" class="Symbol">{</a> <a id="7054" href="Relation.Binary.Structures.html#1887" class="Field">isEquivalence</a> <a id="7068" class="Symbol">=</a> <a id="7070" href="Data.Char.Properties.html#6447" class="Function">≈-isEquivalence</a>
<a id="7088" class="Symbol">;</a> <a id="7090" href="Relation.Binary.Structures.html#1921" class="Field Operator">_≟_</a> <a id="7104" class="Symbol">=</a> <a id="7106" href="Data.Char.Properties.html#5615" class="Function Operator">_≈?_</a>
<a id="7113" class="Symbol">}</a>
<a id="7115" class="Symbol">{-#</a> <a id="7119" class="Keyword">WARNING_ON_USAGE</a> <a id="7136" class="Pragma">≈-isDecEquivalence</a>
<a id="7155" class="String">"Warning: ≈-isDecEquivalence was deprecated in v1.5.
Please use Propositional Equality's isDecEquivalence instead."</a>
<a id="7271" class="Symbol">#-}</a>
<a id="≈-decSetoid"></a><a id="7276" href="Data.Char.Properties.html#7276" class="Function">≈-decSetoid</a> <a id="7288" class="Symbol">:</a> <a id="7290" href="Relation.Binary.Bundles.html#1391" class="Record">DecSetoid</a> <a id="7300" class="Symbol">_</a> <a id="7302" class="Symbol">_</a>
<a id="7304" href="Data.Char.Properties.html#7276" class="Function">≈-decSetoid</a> <a id="7316" class="Symbol">=</a> <a id="7318" class="Keyword">record</a>
<a id="7327" class="Symbol">{</a> <a id="7329" href="Relation.Binary.Bundles.html#1523" class="Field">isDecEquivalence</a> <a id="7346" class="Symbol">=</a> <a id="7348" href="Data.Char.Properties.html#6980" class="Function">≈-isDecEquivalence</a>
<a id="7369" class="Symbol">}</a>
<a id="7371" class="Symbol">{-#</a> <a id="7375" class="Keyword">WARNING_ON_USAGE</a> <a id="7392" class="Pragma">≈-decSetoid</a>
<a id="7404" class="String">"Warning: ≈-decSetoid was deprecated in v1.5.
Please use Propositional Equality's decSetoid instead."</a>
<a id="7506" class="Symbol">#-}</a>
<a id="≡-setoid"></a><a id="7511" href="Data.Char.Properties.html#7511" class="Function">≡-setoid</a> <a id="7520" class="Symbol">:</a> <a id="7522" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="7529" class="Symbol">_</a> <a id="7531" class="Symbol">_</a>
<a id="7533" href="Data.Char.Properties.html#7511" class="Function">≡-setoid</a> <a id="7542" class="Symbol">=</a> <a id="7544" href="Data.Char.Properties.html#1602" class="Function">setoid</a>
<a id="7551" class="Symbol">{-#</a> <a id="7555" class="Keyword">WARNING_ON_USAGE</a> <a id="7572" class="Pragma">≡-setoid</a>
<a id="7581" class="String">"Warning: ≡-setoid was deprecated in v1.5.
Please use setoid instead."</a>
<a id="7652" class="Symbol">#-}</a>
<a id="≡-decSetoid"></a><a id="7657" href="Data.Char.Properties.html#7657" class="Function">≡-decSetoid</a> <a id="7669" class="Symbol">:</a> <a id="7671" href="Relation.Binary.Bundles.html#1391" class="Record">DecSetoid</a> <a id="7681" class="Symbol">_</a> <a id="7683" class="Symbol">_</a>
<a id="7685" href="Data.Char.Properties.html#7657" class="Function">≡-decSetoid</a> <a id="7697" class="Symbol">=</a> <a id="7699" href="Data.Char.Properties.html#1651" class="Function">decSetoid</a>
<a id="7709" class="Symbol">{-#</a> <a id="7713" class="Keyword">WARNING_ON_USAGE</a> <a id="7730" class="Pragma">≡-decSetoid</a>
<a id="7742" class="String">"Warning: ≡-decSetoid was deprecated in v1.5.
Please use decSetoid instead."</a>
<a id="7819" class="Symbol">#-}</a>
<a id="<-isStrictPartialOrder-≈"></a><a id="7824" href="Data.Char.Properties.html#7824" class="Function"><-isStrictPartialOrder-≈</a> <a id="7849" class="Symbol">:</a> <a id="7851" href="Relation.Binary.Structures.html#3950" class="Record">IsStrictPartialOrder</a> <a id="7872" href="Data.Char.Base.html#1260" class="Function Operator">_≈_</a> <a id="7876" href="Data.Char.Base.html#1415" class="Function Operator">_<_</a>
<a id="7880" href="Data.Char.Properties.html#7824" class="Function"><-isStrictPartialOrder-≈</a> <a id="7905" class="Symbol">=</a> <a id="7907" href="Relation.Binary.Construct.On.html#3981" class="Function">On.isStrictPartialOrder</a> <a id="7931" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a> <a id="7935" href="Data.Nat.Properties.html#10374" class="Function">ℕₚ.<-isStrictPartialOrder</a>
<a id="7961" class="Symbol">{-#</a> <a id="7965" class="Keyword">WARNING_ON_USAGE</a> <a id="7982" class="Pragma"><-isStrictPartialOrder-≈</a>
<a id="8007" class="String">"Warning: <-isStrictPartialOrder-≈ was deprecated in v1.5.
Please use <-isStrictPartialOrder instead."</a>
<a id="8110" class="Symbol">#-}</a>
<a id="<-isStrictTotalOrder-≈"></a><a id="8115" href="Data.Char.Properties.html#8115" class="Function"><-isStrictTotalOrder-≈</a> <a id="8138" class="Symbol">:</a> <a id="8140" href="Relation.Binary.Structures.html#6539" class="Record">IsStrictTotalOrder</a> <a id="8159" href="Data.Char.Base.html#1260" class="Function Operator">_≈_</a> <a id="8163" href="Data.Char.Base.html#1415" class="Function Operator">_<_</a>
<a id="8167" href="Data.Char.Properties.html#8115" class="Function"><-isStrictTotalOrder-≈</a> <a id="8190" class="Symbol">=</a> <a id="8192" href="Relation.Binary.Construct.On.html#4950" class="Function">On.isStrictTotalOrder</a> <a id="8214" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a> <a id="8218" href="Data.Nat.Properties.html#10586" class="Function">ℕₚ.<-isStrictTotalOrder</a>
<a id="8242" class="Symbol">{-#</a> <a id="8246" class="Keyword">WARNING_ON_USAGE</a> <a id="8263" class="Pragma"><-isStrictTotalOrder-≈</a>
<a id="8286" class="String">"Warning: <-isStrictTotalOrder-≈ was deprecated in v1.5.
Please use <-isStrictTotalOrder instead."</a>
<a id="8385" class="Symbol">#-}</a>
<a id="<-strictPartialOrder-≈"></a><a id="8390" href="Data.Char.Properties.html#8390" class="Function"><-strictPartialOrder-≈</a> <a id="8413" class="Symbol">:</a> <a id="8415" href="Relation.Binary.Bundles.html#4108" class="Record">StrictPartialOrder</a> <a id="8434" class="Symbol">_</a> <a id="8436" class="Symbol">_</a> <a id="8438" class="Symbol">_</a>
<a id="8440" href="Data.Char.Properties.html#8390" class="Function"><-strictPartialOrder-≈</a> <a id="8463" class="Symbol">=</a> <a id="8465" href="Relation.Binary.Construct.On.html#6309" class="Function">On.strictPartialOrder</a> <a id="8487" href="Data.Nat.Properties.html#10759" class="Function">ℕₚ.<-strictPartialOrder</a> <a id="8511" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a>
<a id="8515" class="Symbol">{-#</a> <a id="8519" class="Keyword">WARNING_ON_USAGE</a> <a id="8536" class="Pragma"><-strictPartialOrder-≈</a>
<a id="8559" class="String">"Warning: <-strictPartialOrder-≈ was deprecated in v1.5.
Please use <-strictPartialOrder instead."</a>
<a id="8658" class="Symbol">#-}</a>
<a id="<-strictTotalOrder-≈"></a><a id="8663" href="Data.Char.Properties.html#8663" class="Function"><-strictTotalOrder-≈</a> <a id="8684" class="Symbol">:</a> <a id="8686" href="Relation.Binary.Bundles.html#6928" class="Record">StrictTotalOrder</a> <a id="8703" class="Symbol">_</a> <a id="8705" class="Symbol">_</a> <a id="8707" class="Symbol">_</a>
<a id="8709" href="Data.Char.Properties.html#8663" class="Function"><-strictTotalOrder-≈</a> <a id="8730" class="Symbol">=</a> <a id="8732" href="Relation.Binary.Construct.On.html#7045" class="Function">On.strictTotalOrder</a> <a id="8752" href="Data.Nat.Properties.html#10895" class="Function">ℕₚ.<-strictTotalOrder</a> <a id="8774" href="Data.Char.Base.html#1123" class="Primitive">toℕ</a>
<a id="8778" class="Symbol">{-#</a> <a id="8782" class="Keyword">WARNING_ON_USAGE</a> <a id="8799" class="Pragma"><-strictTotalOrder-≈</a>
<a id="8820" class="String">"Warning: <-strictTotalOrder-≈ was deprecated in v1.5.
Please use <-strictTotalOrder instead."</a>
<a id="8915" class="Symbol">#-}</a>
</pre></body></html>