chore: upstream Lean.MVarId.applyConst (#458)

leanprover-community · Dec 15, 2023 · 9f8e3f5 · 9f8e3f5
1 parent d76a7e6
commit 9f8e3f5
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Std/Lean/Meta/Basic.lean b/Std/Lean/Meta/Basic.lean
@@ -328,6 +328,10 @@ annotations. -/
 def getTypeCleanup (mvarId : MVarId) : MetaM Expr :=
   return (← instantiateMVars (← mvarId.getType)).cleanupAnnotations
 
+/-- Short-hand for applying a constant to the goal. -/
+def applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
+  mvar.apply (← mkConstWithFreshMVarLevels c) cfg
+
 end MVarId