equal
deleted
inserted
replaced
17 default |
17 default |
18 term |
18 term |
19 |
19 |
20 types |
20 types |
21 bool 0 |
21 bool 0 |
|
22 letbinds, letbind 0 |
22 |
23 |
23 arities |
24 arities |
24 fun :: (term, term) term |
25 fun :: (term, term) term |
25 bool :: term |
26 bool :: term |
26 |
27 |
41 All :: "('a => bool) => bool" (binder "! " 10) |
42 All :: "('a => bool) => bool" (binder "! " 10) |
42 Ex :: "('a => bool) => bool" (binder "? " 10) |
43 Ex :: "('a => bool) => bool" (binder "? " 10) |
43 Ex1 :: "('a => bool) => bool" (binder "?! " 10) |
44 Ex1 :: "('a => bool) => bool" (binder "?! " 10) |
44 |
45 |
45 Let :: "['a, 'a => 'b] => 'b" |
46 Let :: "['a, 'a => 'b] => 'b" |
46 "@Let" :: "[idt, 'a, 'b] => 'b" ("(let _ = (2_)/ in (2_))" 10) |
47 "_bind" :: "[idt, 'a] => letbind" ("(2_ =/ _)" 10) |
|
48 "" :: "letbind => letbinds" ("_") |
|
49 "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
|
50 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
47 |
51 |
48 (* Alternative Quantifiers *) |
52 (* Alternative Quantifiers *) |
49 |
53 |
50 "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10) |
54 "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10) |
51 "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10) |
55 "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10) |
70 translations |
74 translations |
71 "ALL xs. P" => "! xs. P" |
75 "ALL xs. P" => "! xs. P" |
72 "EX xs. P" => "? xs. P" |
76 "EX xs. P" => "? xs. P" |
73 "EX! xs. P" => "?! xs. P" |
77 "EX! xs. P" => "?! xs. P" |
74 "x ~= y" == "~ (x = y)" |
78 "x ~= y" == "~ (x = y)" |
75 "let x = s in t" == "Let(s, %x. t)" |
79 "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" |
76 |
80 "let x = a in e" == "Let(a, %x. e)" |
77 |
81 |
78 rules |
82 rules |
79 |
83 |
80 eq_reflection "(x=y) ==> (x==y)" |
84 eq_reflection "(x=y) ==> (x==y)" |
81 |
85 |