@@ -0,0 +1,36 @@
1+> module MyOrd
2+
3+An alternative Ord instance for Nats, with an explicit name "myord"
4+for the dictionary:
5+
6+> instance [myord] Ord Nat where
7+> compare O (S n) = GT
8+> compare (S n) O = LT
9+> compare O O = EQ
10+
11+The @{name} syntax below gives an explicit dictionary for the compare function.
12+Here, we're telling it to use the "myord" dictionary. Otherwise, it'd just
13+use the default (unnamed) instance. Note that there can only be one unnamed
14+instance --- they must not overlap.
15+
16+> compare (S x) (S y) = compare @{myord} x y
17+
18+> foo : List Nat
19+> foo = [1,4,2,8,3,7,5,6]
20+
21+Sort foo using the default comparison operator:
22+
23+> test1 : List Nat
24+> test1 = sort foo
25+
26+-- which gives [1,2,3,4,5,6,7,8]
27+
28+Sort foo using the alternative instance. No need for 'sortBy' and other
29+such functions. Hoorah!
30+
31+> test2 : List Nat
32+> test2 = sort @{myord} foo
33+
34+-- which gives [8,7,6,5,4,3,2,1]
35+
36+