equal
deleted
inserted
replaced
12 (** Products **) |
12 (** Products **) |
13 |
13 |
14 (* type definition *) |
14 (* type definition *) |
15 |
15 |
16 consts |
16 consts |
17 Pair_Rep :: "['a, 'b] => ['a, 'b] => bool" |
17 Pair_Rep :: ['a, 'b] => ['a, 'b] => bool |
18 |
18 |
19 defs |
19 defs |
20 Pair_Rep_def "Pair_Rep == (%a b. %x y. x=a & y=b)" |
20 Pair_Rep_def "Pair_Rep == (%a b. %x y. x=a & y=b)" |
21 |
21 |
22 subtype (Prod) |
22 subtype (Prod) |
38 types pttrns |
38 types pttrns |
39 |
39 |
40 syntax |
40 syntax |
41 "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))") |
41 "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))") |
42 |
42 |
43 "@pttrn" :: "[pttrn,pttrns] => pttrn" ("'(_,/_')") |
43 "@pttrn" :: [pttrn,pttrns] => pttrn ("'(_,/_')") |
44 "" :: " pttrn => pttrns" ("_") |
44 "" :: pttrn => pttrns ("_") |
45 "@pttrns" :: "[pttrn,pttrns] => pttrns" ("_,/_") |
45 "@pttrns" :: [pttrn,pttrns] => pttrns ("_,/_") |
46 |
46 |
47 translations |
47 translations |
48 "(x, y, z)" == "(x, (y, z))" |
48 "(x, y, z)" == "(x, (y, z))" |
49 "(x, y)" == "Pair x y" |
49 "(x, y)" == "Pair x y" |
50 |
50 |
67 |
67 |
68 subtype (Unit) |
68 subtype (Unit) |
69 unit = "{p. p = True}" |
69 unit = "{p. p = True}" |
70 |
70 |
71 consts |
71 consts |
72 "()" :: "unit" ("'(')") |
72 "()" :: unit ("'(')") |
73 |
73 |
74 defs |
74 defs |
75 Unity_def "() == Abs_Unit(True)" |
75 Unity_def "() == Abs_Unit(True)" |
76 |
76 |
77 (* start 8bit 1 *) |
77 (* start 8bit 1 *) |