102 inj_def "inj(f) == ! x y. f(x)=f(y) --> x=y" |
102 inj_def "inj(f) == ! x y. f(x)=f(y) --> x=y" |
103 inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |
103 inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |
104 surj_def "surj(f) == ! y. ? x. y=f(x)" |
104 surj_def "surj(f) == ! y. ? x. y=f(x)" |
105 |
105 |
106 (* start 8bit 1 *) |
106 (* start 8bit 1 *) |
|
107 syntax |
|
108 "Ð" :: "['a set, 'a set] => 'a set" (infixl 70) |
|
109 "Ñ" :: "['a set, 'a set] => 'a set" (infixl 65) |
|
110 "Î" :: "['a, 'a set] => bool" (infixl 50) |
|
111 "ñ" :: "['a, 'a set] => bool" (infixl 50) |
|
112 GUnion :: "(('a set)set) => 'a set" ("Ó_" [90] 90) |
|
113 GInter :: "(('a set)set) => 'a set" ("Ò_" [90] 90) |
|
114 GUNION1 :: "['a => 'b set] => 'b set" (binder "Ó " 10) |
|
115 GINTER1 :: "['a => 'b set] => 'b set" (binder "Ò " 10) |
|
116 GINTER :: "[pttrn, 'a set, 'b set] => 'b set" ("(3Ò _Î_./ _)" 10) |
|
117 GUNION :: "[pttrn, 'a set, 'b set] => 'b set" ("(3Ó _Î_./ _)" 10) |
|
118 GBall :: "[pttrn, 'a set, bool] => bool" ("(3Â _Î_./ _)" 10) |
|
119 GBex :: "[pttrn, 'a set, bool] => bool" ("(3Ã _Î_./ _)" 10) |
|
120 |
|
121 translations |
|
122 "x ñ y" == "¿(x : y)" |
|
123 "x Î y" == "(x : y)" |
|
124 "x Ð y" == "x Int y" |
|
125 "x Ñ y" == "x Un y" |
|
126 "ÒX" == "Inter X" |
|
127 "ÓX" == "Union X" |
|
128 "Òx.A" == "INT x.A" |
|
129 "Óx.A" == "UN x.A" |
|
130 "ÒxÎA. B" == "INT x:A. B" |
|
131 "ÓxÎA. B" == "UN x:A. B" |
|
132 "ÂxÎA. P" == "! x:A. P" |
|
133 "ÃxÎA. P" == "? x:A. P" |
107 (* end 8bit 1 *) |
134 (* end 8bit 1 *) |
108 |
135 |
109 end |
136 end |
110 |
137 |
111 ML |
138 ML |