documenting the algebraic hierarchy

Stream: general

[Scott Morrison]

There are some current PRs that that "add to the middle" of the algebraic hierarchy, and we've been observing that it's hard to remember all the bits of infrastructure that should be added when a new typeclass arrives.

[Scott Morrison]

I thought it might be good to have a library note documenting some of this.

[Scott Morrison]

Not necessarily as a "tour" of the algebraic hierarchy, but more of a checklist of things you might want to add when adding new classes, either new leaves, or intermediate steps.

[Scott Morrison]

(Perhaps we could even start linting this?)

[Scott Morrison]

I made a little start on branch#hierarchy_design.

[Scott Morrison]

If anyone would like to have a bash at this, please go ahead!

[Scott Morrison]

I wrote down the things that came up in a recent discussion with Eric, but I'm done for the day.

[Scott Morrison]

Current text is at https://github.com/leanprover-community/mathlib/blob/hierarchy_design/src/algebra/hierarchy_design.lean

[Bryan Gin-ge Chen]

We should definitely have more documentation for this sort of thing! Do other large math libraries in other proof assistants have written guidelines along these lines?

[Bryan Gin-ge Chen]

@Scott Morrison I think what's there can be PR'd (in draft form if you still want more contributions). I'd hate for this effort to be forgotten...

[Scott Morrison]

People must have been working on it. :-)

[Scott Morrison]

(Thanks @Eric Wieser!)

[Scott Morrison]

I am working on it more now.

[Scott Morrison]

#6854, if anyone wants to have a go!