|
1826
|
1 |
syntax
|
|
|
2 |
"Ð" :: "['a set, 'a set] => 'a set" (infixl 70)
|
|
|
3 |
"Ñ" :: "['a set, 'a set] => 'a set" (infixl 65)
|
|
|
4 |
"Î" :: "['a, 'a set] => bool" (infixl 50)
|
|
|
5 |
"ñ" :: "['a, 'a set] => bool" (infixl 50)
|
|
|
6 |
GUnion :: "(('a set)set) => 'a set" ("Ó_" [90] 90)
|
|
|
7 |
GInter :: "(('a set)set) => 'a set" ("Ò_" [90] 90)
|
|
|
8 |
GUNION1 :: "['a => 'b set] => 'b set" (binder "Ó " 10)
|
|
|
9 |
GINTER1 :: "['a => 'b set] => 'b set" (binder "Ò " 10)
|
|
|
10 |
GINTER :: "[pttrn, 'a set, 'b set] => 'b set" ("(3Ò _Î_./ _)" 10)
|
|
|
11 |
GUNION :: "[pttrn, 'a set, 'b set] => 'b set" ("(3Ó _Î_./ _)" 10)
|
|
|
12 |
GBall :: "[pttrn, 'a set, bool] => bool" ("(3Â _Î_./ _)" 10)
|
|
|
13 |
GBex :: "[pttrn, 'a set, bool] => bool" ("(3Ã _Î_./ _)" 10)
|
|
|
14 |
|
|
|
15 |
translations
|
|
|
16 |
"x ñ y" == "¿(x : y)"
|
|
|
17 |
"x Î y" == "(x : y)"
|
|
|
18 |
"x Ð y" == "x Int y"
|
|
|
19 |
"x Ñ y" == "x Un y"
|
|
|
20 |
"ÒX" == "Inter X"
|
|
|
21 |
"ÓX" == "Union X"
|
|
|
22 |
"Òx.A" == "INT x.A"
|
|
|
23 |
"Óx.A" == "UN x.A"
|
|
|
24 |
"ÒxÎA. B" == "INT x:A. B"
|
|
|
25 |
"ÓxÎA. B" == "UN x:A. B"
|
|
|
26 |
"ÂxÎA. P" == "! x:A. P"
|
|
|
27 |
"ÃxÎA. P" == "? x:A. P"
|