chore: move MVarId.note (#507)

leanprover-community · Jan 4, 2024 · 0f6bc5b · 0f6bc5b
1 parent a39499e
commit 0f6bc5b
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/Std/Lean/Meta/Basic.lean b/Std/Lean/Meta/Basic.lean
@@ -328,6 +328,11 @@ where
       else
         return e.hasFVar
 
+/-- Add the hypothesis `h : t`, given `v : t`, and return the new `FVarId`. -/
+def note (g : MVarId) (h : Name) (v : Expr) (t? : Option Expr := .none) :
+    MetaM (FVarId × MVarId) := do
+  (← g.assert h (← match t? with | some t => pure t | none => inferType v) v).intro1P
+
 /-- Get the type the given metavariable after instantiating metavariables and cleaning up
 annotations. -/
 def getTypeCleanup (mvarId : MVarId) : MetaM Expr :=

diff --git a/Std/Tactic/SolveByElim.lean b/Std/Tactic/SolveByElim.lean
@@ -32,11 +32,6 @@ open Std.Tactic
 
 namespace Lean.MVarId
 
-/-- Add the hypothesis `h : t`, given `v : t`, and return the new `FVarId`. -/
-def note (g : MVarId) (h : Name) (v : Expr) (t : Option Expr := .none) :
-    MetaM (FVarId × MVarId) := do
-  (← g.assert h (← t.getDM (inferType v)) v).intro1P
-
 /-- For every hypothesis `h : a ~ b` where a `@[symm]` lemma is available,
 add a hypothesis `h_symm : b ~ a`. -/
 def symmSaturate (g : MVarId) : MetaM MVarId := g.withContext do