exprToSyntax for levels

Stream: lean4

[Eric Wieser]

Is there a version of docs#Lean.Elab.Term.exprToSyntax that works for Level?

[Kyle Miller]

Not that I know of. The trick in exprToSyntax is to return ?m but first assign the expression to the metavariable m. There's no syntax for level metavariables. The pretty printer uses?u for level metavariables as a "quasi-syntax".