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?