structures which should be `Prop`s

Stream: lean4

[Kevin Buzzard]

Am I right in thinking that docs4#CanonicallyOrderedAddMonoid should be a Prop not a Type and that this has happened because of a bug in Lean 4's class command? Or am I missing something? If I'm right, can we lint for this bug until it's fixed?

[Yaël Dillies]

I don't see what you mean. It's data.

[Yaël Dillies]

Maybe you are confused because the only fields it adds to its parents are prop fields?

[James Gallicchio]

In particular, Bot A is Type u, and this class extends Bot, no?

[Kevin Buzzard]

Yeah, I'm wrong: thanks. It's extending the structures, not assuming them. Thanks!

[Yaël Dillies]

The docgen output is quite confusing, I must say. We don't get to see all the fields in one place anymore :sad:

[Henrik Böving]

I see that as an advantage really, when you look up a structure you get to see what makes that structure unique, as opposed to a million fields where you are left wondering whether it is reallyy this structure that you need or another one.

[Kyle Miller]

Can't the documentation indicate which fields are the new ones? Maybe it could either use font color or ordering to tell you which is which?

[Kyle Miller]

It would be cool if you could click on a field and get brought to which parent structure is the one responsible for it.

[James Gallicchio]

Or we could put the full field list behind a dropdown button. I agree with Henrik that for classes far down in the hierarchy I don't really want to know all the parent fields...

[Kevin Buzzard]

(It was the switch from Lean 3 doc style to Lean 4 doc style which caught me out, but I'm not arguing that one is better than the other)

[James Gallicchio]

(and within that expanded box, there could be font difference or some annotation about where each one comes from)

[Eric Wieser]

Yaël Dillies said:

The docgen output is quite confusing, I must say. We don't get to see all the fields in one place anymore :sad:

This isn't a docgen change, this is a new-style structure change