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

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)

Test/Tactic.lean

@@ -0,0 +1 @@
+import Test.Tactic.MotivatedApply

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