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
|
let set Empty = variant[]
let set Unit = record {}
let element pt : Unit = {}
let set Three = variant [ zero : Unit | one : Unit | two : Unit ]
let signature SetWithEquivRelation = theory {
Carrier :: Set,
Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set,
Reflexive :: (x : set-of(Carrier)) -> <set-of(Relation x x)>,
Symmetric :: (x : set-of(Carrier)) (y : set-of(Carrier)) (r : set-of(Relation x y)) -> <set-of(Relation y x)>,
Transitive :: (x : set-of(Carrier)) (y : set-of(Carrier)) (z : set-of(Carrier)) (r : set-of(Relation x y)) (s : set-of(Relation z z)) -> <set-of(Relation y z)>
}
let instance eqThree :: SetWithEquivRelation = {
.Carrier = Three :: Set,
.Relation = for (x: Three) (y: Three),
case x of [ zero. z => case y of [ zero. w => Unit :: Set | one. w => Empty :: Set | two. w => Empty :: Set ]
| one. z => case y of [ zero. w => Empty :: Set | one. w => Unit :: Set | two. w => Empty :: Set ]
| two. z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit :: Set ] ],
.Reflexive = for (x: Three), case x of [ zero. z => <pt> | one. z => <pt> | two. z => <pt> ],
.Symmetric = for (x: Three) (y: Three) (r: set-of(Relation x y)),
case x of [ zero. z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ]
| one. z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ]
| two. z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ]
],
.Transitive = for (x: Three)(y: Three)(z: Three)(r: set-of(Relation x y))(s: set-of(Relation y z)), <pt>
}
// let set Diagonal = record { x : set-of(eqThree .Carrier), y : set-of(eqThree .Carrier), equal : set-of((eqThree .Relation) x y) }
// let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt }
|
