universe polymorphism in Expressions

Stream: new members

[Edward van de Meent]

I was trying to write a command with the functionality suggested in #mathlib4 > All instances satisfied by a type , while keeping the metaprogramming book by the hand, when i realised that i can't find how/if the environment knows that a certain declaration has universe polymorphism... does the ConstantInfo somehow contain this information?

[Marcus Rossel]

I think if ConstantInfo.numLevelParams is 0, you shouldn't have any universe level parameters, so no universe polymorphism.

[Edward van de Meent]

aha!

[Edward van de Meent]

another relevant bit is docs#Lean.Level.param, i think

[Marcus Rossel]

Edward van de Meent said:

another relevant bit is docs#Lean.Level.param, i think

Yeah, I guess that depends on whether you're looking at declarations or Exprs. If you're looking at Exprs, you also need to consider docs#Lean.Level.mvar for polymorphism.

[Edward van de Meent]

i'd hope there are no level mvars in Environment.constants, tho

[Edward van de Meent]

or mvars at all

[Edward van de Meent]

since they're the ones that should have been checked by the kernel

[Marcus Rossel]

Based on this explanation of how elaboration of universe levels works, I believe that's correct.