equal
deleted
inserted
replaced
8 OrdQuant = Ordinal + |
8 OrdQuant = Ordinal + |
9 |
9 |
10 consts |
10 consts |
11 |
11 |
12 (* Ordinal Quantifiers *) |
12 (* Ordinal Quantifiers *) |
13 oall, oex :: "[i, i => o] => o" |
13 oall, oex :: [i, i => o] => o |
14 |
14 |
15 (* Ordinal Union *) |
15 (* Ordinal Union *) |
16 OUnion :: "[i, i => i] => i" |
16 OUnion :: [i, i => i] => i |
17 |
17 |
18 syntax |
18 syntax |
19 |
19 |
20 "@oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10) |
20 "@oall" :: [idt, i, o] => o ("(3ALL _<_./ _)" 10) |
21 "@oex" :: "[idt, i, o] => o" ("(3EX _<_./ _)" 10) |
21 "@oex" :: [idt, i, o] => o ("(3EX _<_./ _)" 10) |
22 "@OUNION" :: "[idt, i, i] => i" ("(3UN _<_./ _)" 10) |
22 "@OUNION" :: [idt, i, i] => i ("(3UN _<_./ _)" 10) |
23 |
23 |
24 translations |
24 translations |
25 |
25 |
26 "ALL x<a. P" == "oall(a, %x. P)" |
26 "ALL x<a. P" == "oall(a, %x. P)" |
27 "EX x<a. P" == "oex(a, %x. P)" |
27 "EX x<a. P" == "oex(a, %x. P)" |