Go backward to Subtyping of Function TypesGo up to TopGo forward to Record Introduction Principle |

- Copy rule for lazy evaluated abstractions also applies when abstractions
are locally defined within a block:
**begin define**I=U_{1}, ...,_{1}**define**I=U_{n}_{n}**in**V**end***=>*[U/I_{1}, ..., U_{1}/I_{n}]V_{n}

- Example:
**begin const**`A`=2,**const**`B`=3

**in begin fun**`F`(`X`:`intexp`) =`X`+`A`+`B`

**in begin const**`A`=4**in**`F`(`A`)+`B`**end**

**end****end***=>*...*=>*(`lambda``X`.`X`+2+3)(4)+3

*Does not apply to eagerly evaluated abstractions!*

Author: Wolfgang Schreiner

Last Modification: May 14, 1998