Test/Main.lean

@@ -55,6 +55,7 @@ def main (args: List String) := do
     ("Serial", Serial.suite env_default),
     ("Tactic/Assign", Tactic.Assign.suite env_default),
     ("Tactic/Prograde", Tactic.Prograde.suite env_default),
+    ("Tactic/Special", Tactic.Special.suite env_default),
   ]
   let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
   LSpec.lspecEachIO [()] (λ () => runTestGroup nameFilter? tests)

Test/Tactic.lean

@@ -1,2 +1,3 @@
 import Test.Tactic.Assign
 import Test.Tactic.Prograde
+import Test.Tactic.Special

Test/Tactic/Special.lean

@@ -0,0 +1,23 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.Special
+
+def test_exact_q : TestT Elab.TermElabM Unit := do
+  let rootExpr ← parseSentence "1 + 2 = 2 + 3"
+  let state0 ← GoalState.create rootExpr
+  let tactic := "exact?"
+  let state1? ← state0.tacticOn (goalId := 0) (tactic := tactic)
+  let .failure messages := state1? | fail "Must fail"
+  checkEq "messages" messages #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."]
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("exact?", test_exact_q),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.Special