Reid Barton
Reid Barton
This should carry a huge warning that it is normally not a sensible definition for `Foldable` instances where `f a` contains fields of types other than `a`, such as a...
Oh, so it does. There is such a lot of noise in the diff that I missed it.
As I mentioned on the PR, this often isn't reasonable at all, since there could be fields not covered by the Foldable instance, such as any field that just has...
I think the actual algorithm here should be: * If the name begins with three or more capital letters followed by non-capital letters, then decapitalize all but the last of...
Note that `hAdd` etc. from core do not follow this convention.
Yeah it's annoying that many of these trivial facts about isomorphic things are special cases of less trivial facts which you would want to prove anyways. For example take "if...
> I've been exploring changing `Type` to `Sort` (almost) everywhere in the category theory library, which seems likely to be a prerequisite for doing this. I'm all for doing this!...
Nice! I saw your HoTT/UF abstract a couple weeks ago. I find it a bit surprising that it's possible to do cellular homology synthetically like this without having a homotopy-invariant...
Another way to handle multiple actions of the same group on the same set is to use type synonyms, for example ```lean def G_with_left_action : Type := G instance :...
> Currently only `group_action` and `sylow` rely on `mul_action`; (semi)modules redefine `has_scalar`, and don't use `mul_action`. So, it should be relatively easy to refactor this. It seems that (now) `semimodule`...