auto ext in docs

Stream: general

[Johan Commelin]

Consider docs#bornology. There lemma docs#bornology.ext is placed above the actual definition of bornology, hence referring to a structure that is not yet defined. I think it would make more sense to place this lemma below the defn of the structure.
Is there a reason that it is placed first?

[Yaël Dillies]

Note that this happens all over the place. See for example instances from bar to foo when bar extends foo.

[Yaël Dillies]

Last time I asked, the answer was "Because they are registered in a random order".

[Eric Wieser]

Yeah, I think the answer is "doc-gen is told by lean that the declarations are in that order"

[Johan Commelin]

It might not be worth it, but I guess that Lean could do a slightly better job here.