Expand basendx comment #4283
Expand basendx comment #4283
Conversation
This is to describe when to look at indexes directly and when not to, in both set.mm and iset.mm.
Reword the text about the index being an implementation detail. Use indices for the plural of index.
We can keep some of the details in the basendx comment but the section header for the extensible structure section does discuss the numeric indices and so we should mention the issue there and link to the more detailed discussion.
That's a good point. I had been meaning to look into that more so thanks for the reminder. The header comment for the "Basic definitions" section (currently 7.1.1 in set.mm and a different number in iset.mm) already discusses the numeric indices and avoiding direct reference to them, so this seems like the place. I think putting a one sentence summary there with a pointer to basendx is probably the way to go (I can elaborate on why but the short summary is that our section headers, when we have them, tend to be pretty introductory and point to comments of specific theorems). I've pushed up an addition intended to address this. |
This is to describe when to look at extensible structure indexes directly and when not to, in both set.mm and iset.mm. For further background see #3235 especially the comment #3235 (comment) which nicely summarizes the situation.
If people want to tackle this another way, speak up. But at least to my eyes the text we have now is pretty confusing about when we do and do not expect to look at these indexes.