From 4a92e655f6515d1c6eaaaa991721f5cfb2774154 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 20 Apr 2024 13:09:41 -0700
Subject: [PATCH] test: Tactic test stub

---
 Pantograph/Tactic/MotivatedApply.lean |  1 +
 Test/Main.lean                        |  2 ++
 Test/Tactic.lean                      |  1 +
 Test/Tactic/MotivatedApply.lean       | 11 +++++++++++
 4 files changed, 15 insertions(+)
 create mode 100644 Test/Tactic.lean
 create mode 100644 Test/Tactic/MotivatedApply.lean

diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
index 50a660f..817942d 100644
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -14,6 +14,7 @@ def collectMotiveArguments (forallBody: Expr): SSet Nat :=
   | .app (.bvar i) _ => SSet.empty.insert i
   | _ => SSet.empty
 
+/-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
 def motivatedApply: Elab.Tactic.Tactic := λ stx => do
   let goal ← Elab.Tactic.getMainGoal
   let nextGoals: List MVarId ← goal.withContext do
diff --git a/Test/Main.lean b/Test/Main.lean
index 1aa1d3d..ae897d4 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -5,6 +5,7 @@ import Test.Library
 import Test.Metavar
 import Test.Proofs
 import Test.Serial
+import Test.Tactic
 
 -- Test running infrastructure
 
@@ -48,6 +49,7 @@ def main (args: List String) := do
     ("Metavar", Metavar.suite env_default),
     ("Proofs", Proofs.suite env_default),
     ("Serial", Serial.suite env_default),
+    ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
   ]
   let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
   LSpec.lspecIO (← runTestGroup name_filter tests)
diff --git a/Test/Tactic.lean b/Test/Tactic.lean
new file mode 100644
index 0000000..4284a41
--- /dev/null
+++ b/Test/Tactic.lean
@@ -0,0 +1 @@
+import Test.Tactic.MotivatedApply
diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean
new file mode 100644
index 0000000..04d7825
--- /dev/null
+++ b/Test/Tactic/MotivatedApply.lean
@@ -0,0 +1,11 @@
+import LSpec
+import Lean
+
+open Lean
+
+namespace Pantograph.Test.Tactic.MotivatedApply
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  []
+
+end Pantograph.Test.Tactic.MotivatedApply