Zulip Chat Archive

Stream: general

Topic: auto ext in docs

Johan Commelin (May 28 2022 at 06:49):

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 (May 28 2022 at 06:53):

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

Yaël Dillies (May 28 2022 at 06:54):

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

Eric Wieser (May 28 2022 at 07:09):

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

Johan Commelin (May 28 2022 at 07:10):

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

Last updated: Aug 03 2023 at 10:10 UTC