doc-gen ClosureOperator issue

Stream: mathlib4

[Kevin Buzzard]

I wanted to check the definition of docs#ClosureOperator , but on firefox I see this:

structure ClosureOperator (α : Type u_1) [inst : Preorder α] extends OrderHom :
Type u_1
[axioms...]

which suppresses precisely the information I wanted to see: going to source you see that it extends α →o α. Is this a bug in doc-gen or is there something wrong with my set-up?

[Henrik Böving]

Is the funny arrow an order hom? The part of doc-gen that figures out what you extend from is not based on syntax. It instead figures out the names of the stuff that the elaborator has decided the structure is extending from so there is no delaboration going on right now

[Henrik Böving]

I don't quite know if I can recover the two alpha parameters from the information that the elaborator hands me out trivially but that might be worth a check

[Kevin Buzzard]

Yes, funny arrow "arrow with an o" mean "o-preserving map" and o is short for order. From doc-gen I couldn't tell if it was an order-hom from alpha to alpha, or from alpha to nat or from Prop to alpha or whatever. Then you actually read the axioms and you can figure it out but somehow I was hoping it would be given to me on a plate.

[Henrik Böving]

Right. I'll have a look whether the elaborator easily gives me information about this tomorrow. If not it'll probably take a while until I figure out how to do it

[Eric Wieser]

I guess after you find out Bar extends Foo you could look at the type of Bar.toFoo?

[Eric Wieser]

Does lean4 still have the feature that lets you rename base class projections?

[Kyle Miller]

Just wanted to mention that the extends clause in docgen now gives the precise list of parents, pretty printed with all their parameters:

image.png

Inherited fields are grayed out like implicit arguments, and you can click on them to see where they come from.

[Eric Wieser]

(docs#ClosureOperator)

[Junyan Xu]

In docs#CommRing, if I click on neg_add_cancel, it doesn't jump to anything, although it's already present in Ring, the first parent of CommRing. If I click on add/mul it jumps to Add/Mul. Is it really how extends work under the hood?

[Eric Wieser]

I think this is some nested structure weirdness

[Eric Wieser]

Ring.neg_add_cancel really is the name of the projection, but it's morally a copy of AddGroup.neg_add_cancel

[Eric Wieser]

It looks like the links are taking the literal approach but the shading is taking the moral approach

[Kyle Miller]

Thanks for testing, it seems to be using the wrong projection function when linkifying. It's not meant to expose any of the details of how structures are actually represented.

[Floris van Doorn]

Nice!

[Notification Bot]

6 messages were moved from this topic to #lean4 > #print command for structures by Kyle Miller.