On Tue, 18 Feb 2020 at 14:18, James Cook <jc...@cs.berkeley.edu> wrote: > Narrow comment: "except its interpretation" would make more sense to > me than "but does not include its interpretation"; the latter feels > like a bit of a contradiction (and is longer). > > Broader comment: Any reason for this proposal, beyond trying to > eliminate some redundancy? > > - Falsifian
For the narrow comment, it's potato potato IMO. It's not contradictory, it's a definition. For the broad one, as indicated in the proposal's own comment, R217 controls interpretations of higher-powered rules when lower-powered rules provide definitions or similar. Without that, we arguably need to ignore lower-powered rules completely when interpreting higher-powered ones. The worst-case logical extension would be that even something like dependent actions, where a rule explicitly opens the door to lower-powered ones providing definitions, wouldn't work. I don't think that's the case, but I'd rather be completely explicit about it. -Alexis
