-
Notifications
You must be signed in to change notification settings - Fork 0
/
ord.ya
38 lines (28 loc) · 1.01 KB
/
ord.ya
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
package ord
import bool
where
type Ordering {
LT,
EQ,
GT,
}
type Ord (A: Type) {
New (cmp: ∀ (a b : A) -> Ordering)
}
def Ord.compare (0 A : Type) (ord: Ord A) (a b : A): Ordering
= (case ord) (λ _ => Ordering) (λ cmp => cmp a b)
def Ordering.eql (a b: Ordering): Bool
= (case a) (λ _ => Bool)
((case b) (λ _ => Bool) Bool.True Bool.False Bool.False)
((case b) (λ _ => Bool) Bool.False Bool.True Bool.False)
((case b) (λ _ => Bool) Bool.False Bool.False Bool.True)
def Ord.lth (0 A: Type) (ord: Ord A) (a b: A): Bool
= Ordering.eql (Ord.compare A ord a b) Ordering.LT
def Ord.eql (0 A: Type) (ord: Ord A) (a b: A): Bool
= Ordering.eql (Ord.compare A ord a b) Ordering.EQ
def Ord.gth (0 A: Type) (ord: Ord A) (a b: A): Bool
= Ordering.eql (Ord.compare A ord a b) Ordering.GT
def Ord.lte (0 A: Type) (ord: Ord A) (a b: A): Bool
= Bool.or (Ord.eql A ord a b) (Ord.lth A ord a b)
def Ord.gte (0 A: Type) (ord: Ord A) (a b: A): Bool
= Bool.or (Ord.eql A ord a b) (Ord.gth A ord a b)