Get all level mvars in Expr

Stream: Is there code for X?

[Marcus Rossel]

Is there a way to obtain all universe level mvars contained in a given Expr? So something like Expr.getLMVars : Expr -> List (LMVarId)?

[Kyle Miller]

I'm not aware of something that collects level metavariables, but there's docs#Lean.MetavarContext.levelMVarToParam to convert them to fresh level parameters.

docs#Lean.Elab.Term.levelMVarToParam is an example usage.