Solve level mvars in an expression

Stream: metaprogramming / tactics

[Leni Aniva]

If we have an expression e with level mvars, and we know that its type must conform to t, is there a way to solve and assign all level mvars in e? I know that there's isLevelDefEq, but I don't know how can I invoke it in this context.

[Aaron Liu]

maybe check?

[Leni Aniva]

Aaron Liu said:

maybe check?

that was perfect! thank you

[Aaron Liu]

or you could infer the type, infer the universe, and then check level defeq

[Aaron Liu]

but that sounds a lot more complicated

[Aaron Liu]

and it could also miss some metavariables so I guess the only way to do it is check after all