mcb
mcb copied to clipboard
math-comp
Mathematical Components (the Book)
The link http://math-comp.github.io/math-comp/htmldoc/libgraph.html is broken. It seems to me that the correct link is https://math-comp.github.io/htmldoc/libgraph.html (took it from the math-comp github page).
comment search in snippets because it is too slow for jscoq and leave warning in example in ch2.v/ch2.html. Search (odd _). Search eq odd -coprime. should be kind of (*...
My understanding is that this provides definition-time partial evaluation and that using the specialised programs is more efficient but it would be nice to see this pattern not just used...
- 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...
`Eval compute in tnth [tuple 1; 2; 3] (sub_ord 1).` I think this example (provided by Emilio Jesús Gallego Arias) might be added to the first part of book where...
I think a (sub)chapter about differences between coercions and canonical structures might be added somewhere after Chapter 6.3. I think content may be built on 1-2 examples of coercions from...
The first lemma of Section 6.5: ```Coq Lemma eqP (T : eqType) : Equality.axiom (@Equality.op T). ``` With custom defined `Equality` module in 6.4, it will fail with ``` T...
Here is the code from the book ```Coq Inductive phantom (T : Type) (p : T) := Phantom. Definition set_of (T : eqType) (_ : phantom Type (Equality.sort T)) :=...
In Section 6.2 (Type inference by example) on p. 117, `id` and `idfun` are interleavingly used as names of the same function. Only one of them should be used for...
https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/reading.20mathcomp.20book It should be ```coq Coercion nat_of_ord n (i : 'I_n) := let: @Ordinal _ m _ := i in m. ```
