41 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
41 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
42 Inv :: "('a => 'b) => ('b => 'a)" |
42 Inv :: "('a => 'b) => ('b => 'a)" |
43 |
43 |
44 (* Binders *) |
44 (* Binders *) |
45 |
45 |
46 Eps :: "('a => bool) => 'a" (binder "@" 10) |
46 Eps :: "('a => bool) => 'a" |
47 All :: "('a => bool) => bool" (binder "! " 10) |
47 All :: "('a => bool) => bool" (binder "! " 10) |
48 Ex :: "('a => bool) => bool" (binder "? " 10) |
48 Ex :: "('a => bool) => bool" (binder "? " 10) |
49 Ex1 :: "('a => bool) => bool" (binder "?! " 10) |
49 Ex1 :: "('a => bool) => bool" (binder "?! " 10) |
50 Let :: "['a, 'a => 'b] => 'b" |
50 Let :: "['a, 'a => 'b] => 'b" |
51 |
51 |
52 (* Infixes *) |
52 (* Infixes *) |
53 |
53 |
54 o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) |
54 o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) |
55 "=" :: "['a, 'a] => bool" (infixl 50) |
55 "=" :: "['a, 'a] => bool" (infixl 50) |
56 (*"~=" :: "['a, 'a] => bool" (infixl 50)*) |
|
57 "&" :: "[bool, bool] => bool" (infixr 35) |
56 "&" :: "[bool, bool] => bool" (infixr 35) |
58 "|" :: "[bool, bool] => bool" (infixr 30) |
57 "|" :: "[bool, bool] => bool" (infixr 30) |
59 "-->" :: "[bool, bool] => bool" (infixr 25) |
58 "-->" :: "[bool, bool] => bool" (infixr 25) |
60 |
59 |
61 (* Overloaded Constants *) |
60 (* Overloaded Constants *) |
71 |
70 |
72 syntax |
71 syntax |
73 |
72 |
74 "~=" :: "['a, 'a] => bool" (infixl 50) |
73 "~=" :: "['a, 'a] => bool" (infixl 50) |
75 |
74 |
|
75 "@Eps" :: "[pttrn,bool] => 'a" ("(3@ _./ _)" 10) |
|
76 |
76 (* Alternative Quantifiers *) |
77 (* Alternative Quantifiers *) |
77 |
78 |
78 "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10) |
79 "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10) |
79 "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10) |
80 "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10) |
80 "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10) |
81 "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10) |
81 |
82 |
82 (* Let expressions *) |
83 (* Let expressions *) |
83 |
84 |
84 "_bind" :: "[idt, 'a] => letbind" ("(2_ =/ _)" 10) |
85 "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
85 "" :: "letbind => letbinds" ("_") |
86 "" :: "letbind => letbinds" ("_") |
86 "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
87 "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
87 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
88 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
88 |
89 |
89 (* Case expressions *) |
90 (* Case expressions *) |
93 "" :: "case_syn => cases_syn" ("_") |
94 "" :: "case_syn => cases_syn" ("_") |
94 "@case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
95 "@case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
95 |
96 |
96 translations |
97 translations |
97 "x ~= y" == "~ (x = y)" |
98 "x ~= y" == "~ (x = y)" |
|
99 "@ x.b" == "Eps(%x.b)" |
98 "ALL xs. P" => "! xs. P" |
100 "ALL xs. P" => "! xs. P" |
99 "EX xs. P" => "? xs. P" |
101 "EX xs. P" => "? xs. P" |
100 "EX! xs. P" => "?! xs. P" |
102 "EX! xs. P" => "?! xs. P" |
101 "_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
103 "_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
102 "let x = a in e" == "Let a (%x. e)" |
104 "let x = a in e" == "Let a (%x. e)" |