Cross Reference: /hets/HasCASL/test/Subtype.hascasl
Subtype.hascasl revision 6b7d53eb1a93b9a9d7e3ce48964128fcd142fe53
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
0N/Avars a: Type; b: Type
0N/Atype i a b, Inj a b < a -> b
0N/Avars a: Type; b < a
292N/Aop twice: (a ->? b) -> (a ->? b)
0N/A
0N/Avars f: a ->? b; x: a
0N/A. twice f x = f (f x)
0N/A
292N/Avars a: Type; b: Type
292N/Atype Inj a b = {f: a -> b . forall x, y: a . f x = f y => x = y}
292N/A
292N/Avars a, b: Type; a < b
0N/Aop down: b ->? a
0N/Avar y: b; x: a
0N/A. down y = x
292N/A
292N/Aop up: a -> b
292N/A. down (up x : b) = x
292N/A. def (down (y : b) : a) => up (down y : a) = y
292N/A
292N/Avars c: Type; b < c
292N/A
292N/Avar x: a
292N/A. up (up x : b) = up x : c
292N/A. up (x: a) = x: b
292N/A
0N/Avars c, d, e, f; c < e; d < f
0N/Aforall f: e -> f . up : e ->? f = \ x : e . f x
0N/Aforall f: e ->? d . up f : c ->? f = \ x : c . up (f (up x))
0N/Aforall x: c; y: d . up (x, y) : e * f = (up x, up y)
0N/A