Updated Featherweight Defenders document available

Richard Warburton richard.warburton at gmail.com
Fri Dec 2 17:48:41 PST 2011


On 03/12/11 01:40, Brian Goetz wrote:
> Yes, this notational trick -- where sometimes a variable is free, and 
> sometimes is bound, and the reader has to tell the difference -- is 
> common in many formal models.  In R-IntfSuper, i is a free variable, 
> so the rule defines sres(C, I_i) simultaneously for ALL I_i that are 
> superinterfaces of C.
>
> In the other example you cite, i is bound by the union quantifier, so 
> it is not a free variable.

Just to clarify - I wasn't claiming you had made a mistake, simply that 
the model would be easier to read if you didn't have two variables with 
the same name in the same rule.  Small difference either way, thanks for 
addressing the issue.

regards,

   Richard


More information about the lambda-dev mailing list