Pantograph/Library.lean

@@ -169,14 +169,14 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
   runTermElabM do
     state.restoreElabM
     state.tryTacticM goalId $ Tactic.evalHave binderName.toName type
-@[export pantograph_goal_evaluate_m]
+@[export pantograph_goal_try_define_m]
-protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do
+protected def GoalState.tryDefine (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do
   let expr ← match (← Compile.parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   runTermElabM do
     state.restoreElabM
-    state.tryTacticM goalId (Tactic.evaluate binderName.toName expr)
+    state.tryTacticM goalId (Tactic.evalDefine binderName.toName expr)
 @[export pantograph_goal_let_m]
 def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
   runTermElabM <| state.tryLet goalId binderName type

Pantograph/Tactic/Prograde.lean

@@ -5,19 +5,22 @@ open Lean
 
 namespace Pantograph.Tactic
 
-def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
+/-- Introduces a fvar to the current mvar -/
-  let goal ← Elab.Tactic.getMainGoal
+def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do
-  let nextGoals ← goal.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.define
-    let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
+  let type ← Meta.inferType expr
-    let type ← Meta.inferType expr
 
-    let mvarUpstream ← Meta.withLetDecl binderName type expr λ _ => do
+  Meta.withLetDecl binderName type expr λ fvar => do
-      let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+    let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
-        (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
+      (← mvarId.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
-      goal.assign mvarUpstream
+    mvarId.assign mvarUpstream
-      pure mvarUpstream
+    pure (fvar.fvarId!, mvarUpstream.mvarId!)
-    pure [mvarUpstream.mvarId!]
+
-  Elab.Tactic.setGoals nextGoals
+def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
+  let (_, mvarId) ← define goal binderName expr
+  Elab.Tactic.setGoals [mvarId]
 
 structure BranchResult where
   fvarId?: Option FVarId := .none

Test/Tactic/Prograde.lean

@@ -32,7 +32,7 @@ def test_eval : TestT Elab.TermElabM Unit := do
       ],
       target,
     })
-    let tactic := Tactic.evaluate `h2 e
+    let tactic := Tactic.evalDefine `h2 e
     let m := .mvar ⟨uniq 13⟩
     let [newGoal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number"
     addTest $ LSpec.test "goals after" ((← toCondensedGoal newGoal).devolatilize == {
@@ -73,7 +73,7 @@ def test_proof_eval : TestT Elab.TermElabM Unit := do
 
   let evalBind := "y"
   let evalExpr := "Or.inl h"
-  let state2 ← match ← state1.tryEvaluate (goalId := 0) (binderName := evalBind) (expr := evalExpr) with
+  let state2 ← match ← state1.tryDefine (goalId := 0) (binderName := evalBind) (expr := evalExpr) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString