Infer/synthesize level metavariables

Stream: metaprogramming / tactics

[Chase Norman]

I have an Expr with Level metavariables, and I would like to infer their values, just as is done during elaboration. I tracked down the function Lean.Elab.Term.synthesizeSyntheticMVars, but the pendingMVars list does not contain Level mvars (also, the TermElabM is required). Is there a function to perform this operation?

[Kyle Miller]

When you say it has level metavariables, do you mean you've been creating an Expr with fresh level metavariables whenever you needed them, and then you want to have unification solve for them all?

If so, you can try Meta.check, which unifies metavariables as a side effect. This is conceptually the correct way to go.

Regarding synthesizeSyntheticMVars, this is specifically for expression metavariables that the elaborator will run some code to synthesize an expression from the type alone. For example, coercions, typeclasess, tactic scripts, and so on. It's for postponed elaboration.

Generally inference of e.g. implicit arguments is done through unification instead.