Zulip Chat Archive

Stream: general

Topic: documenting the algebraic hierarchy


view this post on Zulip Scott Morrison (Mar 22 2021 at 23:28):

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.

view this post on Zulip Scott Morrison (Mar 22 2021 at 23:28):

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

view this post on Zulip Scott Morrison (Mar 22 2021 at 23:29):

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.

view this post on Zulip Scott Morrison (Mar 22 2021 at 23:29):

(Perhaps we could even start linting this?)

view this post on Zulip Scott Morrison (Mar 22 2021 at 23:29):

I made a little start on branch#hierarchy_design.

view this post on Zulip Scott Morrison (Mar 22 2021 at 23:29):

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

view this post on Zulip Scott Morrison (Mar 22 2021 at 23:30):

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

view this post on Zulip Scott Morrison (Mar 22 2021 at 23:30):

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

view this post on Zulip Bryan Gin-ge Chen (Mar 23 2021 at 01:07):

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?

view this post on Zulip Bryan Gin-ge Chen (Mar 24 2021 at 23:06):

@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...

view this post on Zulip Scott Morrison (Mar 24 2021 at 23:06):

People must have been working on it. :-)

view this post on Zulip Scott Morrison (Mar 24 2021 at 23:09):

(Thanks @Eric Wieser!)

view this post on Zulip Scott Morrison (Mar 24 2021 at 23:09):

I am working on it more now.

view this post on Zulip Scott Morrison (Mar 24 2021 at 23:48):

#6854, if anyone wants to have a go!


Last updated: May 14 2021 at 00:42 UTC