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