mcb
mcb copied to clipboard
math-comp
further corrections(?)
-
More little examples and parentheticals to help the reader check understanding.
-
Again, \C{compute} -> \C{Compute} since the two are not the same (right?) and it is the latter that is being used.
-
I think the syntactic sugar in the definition of same_bool is expanded more like I suggest than like the previous text suggests (even though the resulting functions, of course, are equivalent). Is that so?
-
Experimental rewrite of the paragraphs on implicit argument. Currently, "About cons" does NOT say anything about "implicit" or "maximally inserted" arguments (at least not on my installation). Thus I removed the mention of "About" here (it should be introduced somewhere, maybe in a separate subsection about Evaluate, Search, About and friends). On the other hand, I have added the (A := U) notation for manually providing implicit arguments.
@darijgr I had a little chat with @ybertot and we believe that the best way forward for this PR is that you split into two parts: one containing the minor fixes, typos, etc which can be merged fast, and another one with the last big chunk which requires more thinking, especially on our side (the book was written a long ago, we need to put your change into context to review it).
Thanks again for your contribution.
@gares Done what you said. Now this branch has the relatively straightforward edits, whereas the implicit argument rewrite is at https://github.com/darijgr/mcb/tree/sugg2b .