Get environment entries in the order they were added

Stream: lean4

[Eric Wieser]

Is there a mechanism to determine which of two definitions within the same (current) module was "defined first"? Presumably for the purpose of kernel checking there can be no back-references, and so the olean file ultimately serializes them in order?

[Damiano Testa]

Is looking at the DeclRangeExt too hacky?

[Eric Wieser]

What does that do for auto-generated declarations?

[Damiano Testa]

Auto-generated declarations often have a reference to the syntax that defines them, but I am not sure whether always.

[Damiano Testa]

E.g., if I remember correctly, to_additive is the range of the additive declaration.

[Eric Wieser]

I'm thinking things like _proof_1 etc

[Damiano Testa]

Ah, those may have the same range of their "parent".

[Damiano Testa]

Do you need to know the actual order, or would an order that is "allowed" be good enough?

[Eric Wieser]

Any allowed order is fine

[Eric Wieser]

I want to be certain that the earlier ones cannot depend on the later ones

[Damiano Testa]

So you could inspect whether one constant appears in the other?

[Eric Wieser]

I'd need to do that transitively, which sounds expensive

[Damiano Testa]

Well, if you first use the range and then that, it may not be too much, maybe.

[Damiano Testa]

This was a previous discussion #lean4 > last declaration added to `Environment` and it links to an earlier discussion, although they do not seem to give much more detail.

[Jannis Limperg]

I've also wanted this recently (in my case, to determine the last declaration in a file -- this is surprisingly tricky). Maybe all these threads indicate enough interest that the FRO would take a PR that adds information about the declaration order to the Environment.