From 0bdb41635bb5f406b23ab83814019be0622a4417 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 16 Jun 2025 14:05:05 -0700
Subject: [PATCH] refactor: Use syntax tactic in unit test

---
 Pantograph/Goal.lean | 2 +-
 Test/Common.lean     | 2 ++
 Test/Proofs.lean     | 8 ++++----
 3 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index c1935cb..d0122f5 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -260,6 +260,7 @@ protected def GoalState.tryTacticM
     (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
     (guardMVarErrors : Bool := false)
     : Elab.TermElabM TacticResult := do
+  assert! ¬ (← goal.isAssigned)
   let prevMessageLength := state.coreState.messages.toList.length
   try
     let nextState ← state.step goal tacticM guardMVarErrors
@@ -289,7 +290,6 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str
     (fileName := ← getFileName) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  assert! ¬ (← goal.isAssigned)
   state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true
 
 protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
diff --git a/Test/Common.lean b/Test/Common.lean
index 8a0623e..5c288f7 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -69,6 +69,8 @@ end Condensed
 
 def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]!
 def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic
+def GoalState.tacticOn' (state: GoalState) (goalId: Nat) (tactic: TSyntax `tactic) :=
+  state.tryTacticM (state.get! goalId) (Elab.Tactic.evalTactic tactic) true
 
 def TacticResult.toString : TacticResult → String
   | .success state _messages => s!".success ({state.goals.length} goals)"
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 8326a0e..7f61e16 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -66,15 +66,15 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
     return a
 
 def test_identity: TestM Unit := do
-  let state0 ← GoalState.create (expr := ← parseSentence "∀ (p: Prop), p → p")
-  let tactic := "intro p h"
-  let state1 ← match ← state0.tacticOn 0 tactic with
+  let rootTarget ← Elab.Term.elabTerm (← `(term|∀ (p: Prop), p → p)) .none
+  let state0 ← GoalState.create (expr := rootTarget)
+  let state1 ← match ← state0.tacticOn' 0 (← `(tactic|intro p h)) with
     | .success state _ => pure state
     | other => do
       fail other.toString
       return ()
   let inner := "_uniq.11"
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
+  addTest $ LSpec.check "intro" ((← state1.serializeGoals (options := ← read)).map (·.name) =
     #[inner])
   let state1parent ← state1.withParentContext do
     serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)