From cbf7a661df5dde8f1e781375d8e439ca1884d5eb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Mar 2020 11:31:18 -0700
Subject: [PATCH] feat: add `elabAsFVar`

---
 src/Init/Lean/Elab/Tactic/ElabTerm.lean | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/src/Init/Lean/Elab/Tactic/ElabTerm.lean b/src/Init/Lean/Elab/Tactic/ElabTerm.lean
index 9f9856db08..d6bf27ac27 100644
--- a/src/Init/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Init/Lean/Elab/Tactic/ElabTerm.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Lean.Meta.Tactic.Apply
+import Init.Lean.Meta.Tactic.Assert
 import Init.Lean.Elab.Tactic.Basic
 import Init.Lean.Elab.SyntheticMVars
 
@@ -68,6 +69,29 @@ fun stx => match_syntax stx with
     setGoals (gs' ++ gs)
   | _ => throwUnsupportedSyntax
 
+/--
+  Elaborate `stx`. If it a free variable, return it. Otherwise, assert it, and return the free variable.
+  Note that, the main goal is updated when `Meta.assert` is used in the second case. -/
+def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId := do
+(mvarId, others) ← getMainGoal stx;
+withMVarContext mvarId $ do
+  e ← elabTerm stx none;
+  match e with
+  | Expr.fvar fvarId _ => pure fvarId
+  | _ => do
+    type ← inferType stx e;
+    let intro (userName : Name) (useUnusedNames : Bool) : TacticM FVarId := do {
+      (fvarId, mvarId) ← liftMetaM stx $ do {
+        mvarId ← Meta.assert mvarId userName type e;
+        Meta.intro1 mvarId useUnusedNames
+      };
+      setGoals $ mvarId::others;
+      pure fvarId
+    };
+    match userName? with
+    | none          => intro `h true
+    | some userName => intro userName false
+
 end Tactic
 end Elab
 end Lean