126 "ALL x:A. P" == "Ball(A, %x. P)" |
126 "ALL x:A. P" == "Ball(A, %x. P)" |
127 "EX x:A. P" == "Bex(A, %x. P)" |
127 "EX x:A. P" == "Bex(A, %x. P)" |
128 |
128 |
129 "<x, y, z>" == "<x, <y, z>>" |
129 "<x, y, z>" == "<x, <y, z>>" |
130 "<x, y>" == "Pair(x, y)" |
130 "<x, y>" == "Pair(x, y)" |
131 "%<x,y,zs>.b" == "split(%x <y,zs>.b)" |
131 "%<x,y,zs>.b" == "split(%x <y,zs>.b)" |
132 "%<x,y>.b" == "split(%x y.b)" |
132 "%<x,y>.b" == "split(%x y.b)" |
133 (* The <= direction fails if split has more than one argument because |
133 |
134 ast-matching fails. Otherwise it would work fine *) |
|
135 |
134 |
136 defs |
135 defs |
137 |
136 |
138 (* Bounded Quantifiers *) |
137 (* Bounded Quantifiers *) |
139 Ball_def "Ball(A, P) == ALL x. x:A --> P(x)" |
138 Ball_def "Ball(A, P) == ALL x. x:A --> P(x)" |