mcb
mcb copied to clipboard
math-comp
Mathematical Components (the Book)
does not fit well ch5, `Posz` is out of the scope of the book, still some room for notational aspects of specs. We should talk about that later once we...
The main message of the discussion on the definition of subn seems to be to comment on the impact of the necessary totality of functions. This should be promoted as...
See the suggestions by @mdnahas in the (merged) #11.
Instructions for building the book from source, for typechecking the Coq code from the book, etc.
Hi, Do you guys have any plan to host an HTML version like [SF](https://softwarefoundations.cis.upenn.edu) and [CPDT](http://adam.chlipala.net/cpdt/html/toc.html)? That would be awesome.
Chances are this is not really an issue. It's just an alternative proof for the `stamps` lemma: ```coq Lemma addnBAC m n p : n n (m - n) +...
I found that the explanation of the proof of edivnP on p. 110 is not updated. I read the book version 1.0.2. The proof of edivnP is changed in the...
