Instantiate all delayed mvars

Stream: lean4

[Leni Aniva]

Is there a way to instantiate all delayed mvars in the context which delayed mvars can be deduced?

For example, the type of this expression

@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))

is 2 <= 5, but the raw expression tree of this 2 <= 5 contains delayed mvars of the form

OfNat.ofNat _ 2 _

[Kyle Miller]

instantiateMVars handles delayed assignment metavariables that can be instantiated