equal
deleted
inserted
replaced
285 |
285 |
286 For applications: |
286 For applications: |
287 |
287 |
288 * If the application involves a bounded quantifier, we recurse on |
288 * If the application involves a bounded quantifier, we recurse on |
289 the second argument. If the application is a bounded abstraction, |
289 the second argument. If the application is a bounded abstraction, |
290 we always put an Re/Abs around it (since bounded abstractions |
290 we always put an Rep/Abs around it (since bounded abstractions |
291 always need lifting). Otherwise we recurse on both arguments. |
291 are assumed to always need lifting). Otherwise we recurse on both |
|
292 arguments. |
292 |
293 |
293 For constants: |
294 For constants: |
294 |
295 |
295 * If the constant is (op =), we leave it always unchanged. |
296 * If the constant is (op =), we leave it always unchanged. |
296 Otherwise the type of the constant needs lifting, we put |
297 Otherwise the type of the constant needs lifting, we put |