empty universe levels

Stream: lean4

[Arthur Paulino]

Hi! We have the following axiom in the environment:

unsafe axiom min._at.List.minimum?._spec_1 [] : forall (α : Type.{u}) (inst._@.Init.Data.List.Basic._hyg.5374 : LE.{u} α), (DecidableRel.{succ u} α (LE.le.{u} α inst._@.Init.Data.List.Basic._hyg.5374)) -> α -> α -> α

My question is related to the universe levels for this axiom. The [] means that (val : AxiomVal).levelParams is empty. But then how can Lean know what Type.{u} is if u is not available?

[Leonardo de Moura]

This is an auxiliary declaration created by the code generator. Note that it is marked as unsafe, and we are not checking universes at this point of the compilation.

[Arthur Paulino]

I see, thanks!
What's the role of an unsafe declaration like this?

[Sebastian Ullrich]

It is essentially an IR cache