15 i :: term |
15 i :: term |
16 |
16 |
17 |
17 |
18 consts |
18 consts |
19 |
19 |
20 "0" :: "i" ("0") (*the empty set*) |
20 "0" :: "i" ("0") (*the empty set*) |
21 Pow :: "i => i" (*power sets*) |
21 Pow :: "i => i" (*power sets*) |
22 Inf :: "i" (*infinite set*) |
22 Inf :: "i" (*infinite set*) |
23 |
23 |
24 (* Bounded Quantifiers *) |
24 (* Bounded Quantifiers *) |
25 |
25 |
26 "@Ball" :: "[idt, i, o] => o" ("(3ALL _:_./ _)" 10) |
26 "@Ball" :: "[idt, i, o] => o" ("(3ALL _:_./ _)" 10) |
27 "@Bex" :: "[idt, i, o] => o" ("(3EX _:_./ _)" 10) |
27 "@Bex" :: "[idt, i, o] => o" ("(3EX _:_./ _)" 10) |
28 Ball :: "[i, i => o] => o" |
28 Ball :: "[i, i => o] => o" |
29 Bex :: "[i, i => o] => o" |
29 Bex :: "[i, i => o] => o" |
30 |
30 |
31 (* General Union and Intersection *) |
31 (* General Union and Intersection *) |
32 |
32 |
33 "@INTER" :: "[idt, i, i] => i" ("(3INT _:_./ _)" 10) |
33 "@INTER" :: "[idt, i, i] => i" ("(3INT _:_./ _)" 10) |
34 "@UNION" :: "[idt, i, i] => i" ("(3UN _:_./ _)" 10) |
34 "@UNION" :: "[idt, i, i] => i" ("(3UN _:_./ _)" 10) |
35 Union, Inter :: "i => i" |
35 Union, Inter :: "i => i" |
36 |
36 |
37 (* Variations on Replacement *) |
37 (* Variations on Replacement *) |
38 |
38 |
39 "@Replace" :: "[idt, idt, i, o] => i" ("(1{_ ./ _: _, _})") |
39 "@Replace" :: "[idt, idt, i, o] => i" ("(1{_ ./ _: _, _})") |
40 "@RepFun" :: "[i, idt, i] => i" ("(1{_ ./ _: _})") |
40 "@RepFun" :: "[i, idt, i] => i" ("(1{_ ./ _: _})") |
41 "@Collect" :: "[idt, i, o] => i" ("(1{_: _ ./ _})") |
41 "@Collect" :: "[idt, i, o] => i" ("(1{_: _ ./ _})") |
42 PrimReplace :: "[i, [i, i] => o] => i" |
42 PrimReplace :: "[i, [i, i] => o] => i" |
43 Replace :: "[i, [i, i] => o] => i" |
43 Replace :: "[i, [i, i] => o] => i" |
44 RepFun :: "[i, i => i] => i" |
44 RepFun :: "[i, i => i] => i" |
45 Collect :: "[i, i => o] => i" |
45 Collect :: "[i, i => o] => i" |
46 |
46 |
47 (* Descriptions *) |
47 (* Descriptions *) |
48 |
48 |
49 The :: "(i => o) => i" (binder "THE " 10) |
49 The :: "(i => o) => i" (binder "THE " 10) |
50 if :: "[o, i, i] => i" |
50 if :: "[o, i, i] => i" |
51 |
51 |
52 (* Enumerations of type i *) |
52 (* Enumerations of type i *) |
53 |
53 |
54 "" :: "i => is" ("_") |
54 "" :: "i => is" ("_") |
55 "@Enum" :: "[i, is] => is" ("_,/ _") |
55 "@Enum" :: "[i, is] => is" ("_,/ _") |
56 |
56 |
57 (* Finite Sets *) |
57 (* Finite Sets *) |
58 |
58 |
59 "@Finset" :: "is => i" ("{(_)}") |
59 "@Finset" :: "is => i" ("{(_)}") |
60 Upair, cons :: "[i, i] => i" |
60 Upair, cons :: "[i, i] => i" |
61 succ :: "i => i" |
61 succ :: "i => i" |
62 |
62 |
63 (* Ordered Pairing and n-Tuples *) |
63 (* Ordered Pairing and n-Tuples *) |
64 |
64 |
65 "@Tuple" :: "[i, is] => i" ("<(_,/ _)>") |
65 "@Tuple" :: "[i, is] => i" ("<(_,/ _)>") |
66 Pair :: "[i, i] => i" |
66 Pair :: "[i, i] => i" |
67 fst, snd :: "i => i" |
67 fst, snd :: "i => i" |
68 split :: "[[i,i] => i, i] => i" |
68 split :: "[[i, i] => i, i] => i" |
69 fsplit :: "[[i,i] => o, i] => o" |
69 fsplit :: "[[i, i] => o, i] => o" |
70 |
70 |
71 (* Sigma and Pi Operators *) |
71 (* Sigma and Pi Operators *) |
72 |
72 |
73 "@PROD" :: "[idt, i, i] => i" ("(3PROD _:_./ _)" 10) |
73 "@PROD" :: "[idt, i, i] => i" ("(3PROD _:_./ _)" 10) |
74 "@SUM" :: "[idt, i, i] => i" ("(3SUM _:_./ _)" 10) |
74 "@SUM" :: "[idt, i, i] => i" ("(3SUM _:_./ _)" 10) |
75 "@lam" :: "[idt, i, i] => i" ("(3lam _:_./ _)" 10) |
75 "@lam" :: "[idt, i, i] => i" ("(3lam _:_./ _)" 10) |
76 Pi, Sigma :: "[i, i => i] => i" |
76 Pi, Sigma :: "[i, i => i] => i" |
77 |
77 |
78 (* Relations and Functions *) |
78 (* Relations and Functions *) |
79 |
79 |
80 domain :: "i => i" |
80 domain :: "i => i" |
81 range :: "i => i" |
81 range :: "i => i" |
82 field :: "i => i" |
82 field :: "i => i" |
83 converse :: "i => i" |
83 converse :: "i => i" |
84 Lambda :: "[i, i => i] => i" |
84 Lambda :: "[i, i => i] => i" |
85 restrict :: "[i, i] => i" |
85 restrict :: "[i, i] => i" |
86 |
86 |
87 (* Infixes in order of decreasing precedence *) |
87 (* Infixes in order of decreasing precedence *) |
88 |
88 |
89 "``" :: "[i, i] => i" (infixl 90) (*image*) |
89 "``" :: "[i, i] => i" (infixl 90) (*image*) |
90 "-``" :: "[i, i] => i" (infixl 90) (*inverse image*) |
90 "-``" :: "[i, i] => i" (infixl 90) (*inverse image*) |
91 "`" :: "[i, i] => i" (infixl 90) (*function application*) |
91 "`" :: "[i, i] => i" (infixl 90) (*function application*) |
92 |
92 |
93 (*Except for their translations, * and -> are right-associating infixes*) |
93 (*Except for their translations, * and -> are right and ~: left associative infixes*) |
94 " *" :: "[i, i] => i" ("(_ */ _)" [81, 80] 80) (*Cartesian product*) |
94 " *" :: "[i, i] => i" ("(_ */ _)" [81, 80] 80) (*Cartesian product*) |
95 "Int" :: "[i, i] => i" (infixl 70) (*binary intersection*) |
95 "Int" :: "[i, i] => i" (infixl 70) (*binary intersection*) |
96 "Un" :: "[i, i] => i" (infixl 65) (*binary union*) |
96 "Un" :: "[i, i] => i" (infixl 65) (*binary union*) |
97 "-" :: "[i, i] => i" (infixl 65) (*set difference*) |
97 "-" :: "[i, i] => i" (infixl 65) (*set difference*) |
98 " ->" :: "[i, i] => i" ("(_ ->/ _)" [61, 60] 60) (*function space*) |
98 " ->" :: "[i, i] => i" ("(_ ->/ _)" [61, 60] 60) (*function space*) |
99 "<=" :: "[i, i] => o" (infixl 50) (*subset relation*) |
99 "<=" :: "[i, i] => o" (infixl 50) (*subset relation*) |
100 ":" :: "[i, i] => o" (infixl 50) (*membership relation*) |
100 ":" :: "[i, i] => o" (infixl 50) (*membership relation*) |
101 "~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*) |
101 "~:" :: "[i, i] => o" ("(_ ~:/ _)" [50, 51] 50) (*negated membership relation*) |
102 |
102 |
103 |
103 |
104 translations |
104 translations |
105 "{x, xs}" == "cons(x, {xs})" |
105 "{x, xs}" == "cons(x, {xs})" |
106 "{x}" == "cons(x, 0)" |
106 "{x}" == "cons(x, 0)" |