Fresh universe name

Stream: lean4

[Tomas Skrivan]

What is the best way to create a fresh new name for Level.param name? I want to create a new universe polymorphic declaration. I already have bunch of universe parameters coming from already existing declaration and want to add one more.

[Kyle Miller]

One way is to use the TermElabM monad to keep track of universe levels. You could take a look at the Type* notation in mathlib for a pointer to the relevant functions.

You could also see how this tactic handles transformations of lemmas, adding a new universe level: https://github.com/leanprover-community/mathlib4/blob/2c3ee375d609fb8e22e675d46e5e19a145f10617/Mathlib/Tactic/CategoryTheory/Elementwise.lean#L196

[Tomas Skrivan]

Thanks, mkUnusedName looks good for my use!