On Wed, 19 Feb 2020 at 04:13, Alexis Hunt via agora-discussion <agora-discussion@agoranomic.org> wrote: > 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
Thanks for the explanation. - Falsifian
