Hi, I recently had a closer look at Chapter 7, and here are a few subtle things I stumbled across:
Sect. 7.1: It took me quite a while (and a lot of Find/Check/Print and looking at the source files) to find out that ComRingMixin, even though it takes a proof of commutativity, only constructs a generic ring mixin (using commutativity to obtain the right identity/distribution laws). This was made all the more confusing though the comment that for commutative rings no mixin definition is necessary. Maybe add a sentence to explain that.
Sect 7.3: Here class is just the explicit definition of the second component of the Section variable cT : type. This may be bordering on being pedantic, but to me this sounds like the (given) section variable being defined. How about: Here, class is just a short name for the second component ... ?
Also, matching the presented code snipped against the actual code in choice.v reveals that the base, mixin and sort coercions are only defined later in the Exports module. Incidentally, the sort coercion is needed for class to type check and the local coercion introduced in choice.v for this purpose is suppressed in the html documentation. These discrepancies and the hidden local coercion make it hard to follow the provided patterns.
Sect 7.3: I am not sure strict identities is the best terminology to refer to equality axioms. In particular, since that terminology is not used elsewhere. Moreover understanding the example associative add requires looking up/knowing the definition of associative, which is about 100 pages away.
Sect 7.5: Remark how... I'm pretty sure you want the reader to note this and not make a remark (Well, I now made a remark. :smile: ). Similarly, the last paragraph should maybe start with More generally, ...
That being said, the chapter helped me to better understand the the subtleties of packaging classes. :+1:
gares
commented
5 years ago
Hi, I recently had a closer look at Chapter 7, and here are a few subtle things I stumbled across:
ComRingMixin, even though it takes a proof of commutativity, only constructs a generic ring mixin (using commutativity to obtain the right identity/distribution laws). This was made all the more confusing though the comment that for commutative rings no mixin definition is necessary. Maybe add a sentence to explain that.Here class is just the explicit definition of the second component of the Section variable cT : type. This may be bordering on being pedantic, but to me this sounds like the (given) section variable being defined. How about: Here,classis just a short name for the second component ... ? Also, matching the presented code snipped against the actual code inchoice.vreveals that thebase,mixinandsortcoercions are only defined later in the Exports module. Incidentally, thesortcoercion is needed for class to type check and the local coercion introduced in choice.v for this purpose is suppressed in the html documentation. These discrepancies and the hidden local coercion make it hard to follow the provided patterns.strict identitiesis the best terminology to refer to equality axioms. In particular, since that terminology is not used elsewhere. Moreover understanding the exampleassociative addrequires looking up/knowing the definition of associative, which is about 100 pages away.Remark how...I'm pretty sure you want the reader to note this and not make a remark (Well, I now made a remark. :smile: ). Similarly, the last paragraph should maybe start withMore generally, ...That being said, the chapter helped me to better understand the the subtleties of packaging classes. :+1: