mcb
mcb copied to clipboard
math-comp
Mathematical Components (the Book)
The book mentions CoqIDE, Coqoon and Proof General as tools facilitating interaction with Coq. It should probably mention the VsCoq plugin and the Coq Platform as well.
The following link looks broken: https://github.com/math-comp/mcb/blob/c32cc2cada2c123d44b4f345f3812e3b199d478b/tex/chTypeInference.tex#L240 [Page 118](https://zenodo.org/record/3999478): `Chapter ??`.
The book saids: ``` Inductive ex2 A P Q : Prop := ex_intro2 x of P x & Q x. ``` I guess it should be like this: ``` Inductive...
End of section 8.4 , in the definition of `pack` : provide a type annotation for `m` and explain why `m0` cannot be used as such, as in `Pack (@Class...
See example in section 8.3. For the sake of uniformity, I have removed it from the inline. It is more uniformly uglier.
We use it in section 8.1. I have added a sentence but more might be needed.
The 1st paragraph in section 8.1 is not clear: clarify the discourse about structure vs interface.
As Simon says, the block of notations declarations (LHS, etc) is too dry and deserves a line-per-line comment.