Andres Erbsen

"push" lemmas have often been named like `mul_cos : cos(a)*cos(b) = (cos(a+b) + cos(a-b))/2`, `add_0_r`, `not_not_decidable`. I find that naming scheme very intuitive and helpful, often allowing to skip a...

By "push" lemmas I mean the rules for commuting one operation from outside of other operations to inputs of these operations. Here are some push lemmas for `Z.pow` from the...

I think there is value in having these included even if they are auto-generated for some types. I am guessing that if we counted the uses of `eqListA` from current...

I would like `=` not to be bound to `Logic.eq` in prelude, and perhaps not have `Logic.eq` in prelude at all. Having `=` picked up as `Logic.eq` in files where...

I think `=` is the natural choice for equality even if it does not coincide with `Logic.eq`. I agree that one shouldn't define multiple relations on a type and then...

Thank you for the kind words. I agree that volunteer time and interests are a significant constraint here, and I am aware that many other developers are not as enthusiastic...

Cc @coq/stdlib-maintainers your input would be appreciated (and not all of you are watching this repository).

Could you please say more about the advantages of the proposed system over the current one -- why should we do what you say under "Motivation"? We clearly have different...

@proux01 would you be willing to engage with me on this topic, in a medium of your choice? I see the value of some aspects of this CEP (e.g., cleaning...

~~Could we have this coq-call discussion the week after, on the 12th? I'm unsure whether I'll be able to make it on the 5th, but I would very much like...