Patrick Nicodemus
Patrick Nicodemus
We add some theorems of natural number arithmetic involving pred, S, + , -, < and
I would like feedback on organization and naming. My current plan would just be to borrow the names from ssreflect for whatever lemmas I need.
I suggest some reorganization and renaming in `Structure/Monoidal/Cartesian.v` and `Structure/Monoidal/Cartesian/Cartesian.v`. There are two relations between monoidal products and Cartesian products: 1. Every Cartesian product is a monoidal product. 2. A...
Tl; dr: The category Cat is defined "incorrectly", in particular its setoid hom equivalence relation is wrong (it does not agree with the ZFC definition of equality between functors). I...
From Theory/Functor.v - ``` Class Full `(F : C ⟶ D) := { prefmap {x y} (g : F x ~> F y) : x ~> y; prefmap_respects {x y}...
The generalized rewriting tool is time intensive because it does a lot of unification comparisons on complicated terms. An effective solution seems to be, for every rewrite command, replace every...
This changes the definition of ssqr_diff' so that it does not mutate the inputs. Two tests are added for correctness and to check that it does not mutate the inputs....
The function `Mat.ssqr_diff'` appears to modify its inputs in place without warning. If you try to compute `Mat.ssqr_diff' A B` then this has the side effect `A.(i,j)
This feature arguably falls outside the scope of the library - it is really a problem which is 2 dependencies down the food chain - but I will suggest it...