Pantograph.lean

@@ -125,7 +125,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           pure ( Except.ok (← goalAssign goalState args.goalId expr))
         | .none, .none, .some type, .none, .none => do
           let binderName := args.binderName?.getD ""
-          pure ( Except.ok (← goalState.tryHave args.goalId binderName type))
+          pure ( Except.ok (← goalHave goalState args.goalId binderName type))
         | .none, .none, .none, .some pred, .none => do
           pure ( Except.ok (← goalCalc goalState args.goalId pred))
         | .none, .none, .none, .none, .some true => do

Pantograph/Compile.lean

@@ -2,7 +2,7 @@
 import Pantograph.Protocol
 import Pantograph.Compile.Frontend
 import Pantograph.Compile.Elab
-import Pantograph.Compile.Parse
+
 
 open Lean
 

Pantograph/Compile/Parse.lean

@@ -1,14 +0,0 @@
-import Lean
-
-open Lean
-
-namespace Pantograph.Compile
-
-def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
-  return Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := `term)
-    (input := s)
-    (fileName := "<stdin>")
-
-end Pantograph.Compile

Pantograph/Condensed.lean

@@ -1,42 +0,0 @@
-/- structures for FFI based interface -/
-import Lean
-
-open Lean
-
-namespace Pantograph.Condensed
-
-/-
-These two functions are for user defiend names. For internal names such as
-`_uniq`, it is favourable to use `lean_name_hash_exported` and `lean_name_eq` to
-construct hash maps for Lean names.
--/
-@[export pantograph_str_to_name]
-def strToName (s: String) : Name := s.toName
-@[export pantograph_name_to_str]
-def nameToStr (s: String) : Name := s.toName
-@[export pantograph_name_is_inaccessible]
-def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName
-
--- Mirrors Lean's LocalDecl
-structure LocalDecl where
-  -- Default value is for testing
-  fvarId: FVarId := { name := .anonymous }
-  userName: Name
-
-  -- Normalized expression
-  type : Expr
-  value? : Option Expr := .none
-
-structure Goal where
-  mvarId: MVarId := { name := .anonymous }
-  userName: Name := .anonymous
-  context: Array LocalDecl
-  target: Expr
-
-@[export pantograph_goal_is_lhs]
-def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
-
-
-
-
-end Pantograph.Condensed

Pantograph/Goal.lean

@@ -5,7 +5,6 @@ All the functions starting with `try` resume their inner monadic state.
 -/
 import Pantograph.Protocol
 import Pantograph.Tactic
-import Pantograph.Compile.Parse
 import Lean
 
 def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
@@ -64,16 +63,9 @@ protected def GoalState.mctx (state: GoalState): MetavarContext :=
 protected def GoalState.env (state: GoalState): Environment :=
   state.savedState.term.meta.core.env
 
-@[export pantograph_goal_state_meta_context_of_goal]
-protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do
-  let mvarDecl ← state.mctx.findDecl? mvarId
-  return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
-@[export pantograph_goal_state_meta_state]
-protected def GoalState.metaState (state: GoalState): Meta.State :=
-  state.savedState.term.meta.meta
-
 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
-  mvarId.withContext m |>.run' (← read) state.metaState
+  let metaM := mvarId.withContext m
+  metaM.run' (← read) state.savedState.term.meta.meta
 
 protected def GoalState.withParentContext (state: GoalState) (m: MetaM α): MetaM α := do
   state.withContext state.parentMVar?.get! m
@@ -90,7 +82,6 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac
   state.savedState.restore
   Elab.Tactic.setGoals [goal]
 
-
 private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
   mctxNew.decls.foldl (fun acc mvarId mvarDecl =>
     if let .some prevMVarDecl := mctxOld.decls.find? mvarId then
@@ -278,6 +269,57 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
 
 -- Specialized Tactics
 
+protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  goal.checkNotAssigned `GoalState.tryHave
+  let type ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := type)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  let binderName := binderName.toName
+  try
+    -- Implemented similarly to the intro tactic
+    let nextGoals: List MVarId ← goal.withContext do
+      let type ← Elab.Term.elabType (stx := type)
+      let lctx ← MonadLCtx.getLCtx
+
+      -- The branch goal inherits the same context, but with a different type
+      let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
+
+      -- Create the context for the `upstream` goal
+      let fvarId ← mkFreshFVarId
+      let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
+      let fvar   := mkFVar fvarId
+      let mvarUpstream ←
+        withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
+          Meta.withNewLocalInstances #[fvar] 0 do
+            let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+              (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
+            -- FIXME: May be redundant?
+            let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
+            goal.assign expr
+            pure mvarUpstream
+
+      pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals := nextGoals }
+      },
+      newMVars := nextGoals.toSSet,
+      parentMVar? := .some goal,
+      calcPrevRhs? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
 protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
@@ -477,23 +519,35 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
 protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let recursor ← match (← Compile.parseTermM recursor) with
+  let recursor ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := recursor)
+    (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.execute goalId (tacticM := Tactic.motivatedApply recursor)
 protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let eq ← match (← Compile.parseTermM eq) with
+  let recursor ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := eq)
+    (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.noConfuse eq)
+  state.execute goalId (tacticM := Tactic.noConfuse recursor)
 protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Name) (expr: String) :
       Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let expr ← match (← Compile.parseTermM expr) with
+  let expr ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := expr)
+    (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.evaluate binderName expr)
+  state.execute goalId (tacticM := Tactic.tacticEval binderName expr)
 
 end Pantograph

Pantograph/Library.lean

@@ -180,21 +180,8 @@ def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticRe
 def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult :=
   runTermElabM <| state.tryAssign goalId expr
 @[export pantograph_goal_have_m]
-protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do
+def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
-  let type ← match (← Compile.parseTermM type) with
+  runTermElabM <| state.tryHave goalId binderName type
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  runTermElabM do
-    state.restoreElabM
-    state.execute goalId (Tactic.«have» binderName.toName type)
-@[export pantograph_goal_evaluate_m]
-protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do
-  let type ← match (← Compile.parseTermM type) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  runTermElabM do
-    state.restoreElabM
-    state.execute goalId (Tactic.evaluate binderName.toName type)
 @[export pantograph_goal_let_m]
 def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
   runTermElabM <| state.tryLet goalId binderName type
@@ -217,16 +204,15 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Core
 def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult :=
   runTermElabM <| state.tryNoConfuse goalId eq
 
-inductive SyntheticTactic where
+inductive TacticExecute where
   | congruenceArg
   | congruenceFun
   | congruence
-/-- Executes a synthetic tactic which has no arguments -/
+@[export pantograph_goal_tactic_execute_m]
-@[export pantograph_goal_synthetic_tactic_m]
+def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): CoreM TacticResult :=
-def goalSyntheticTactic (state: GoalState) (goalId: Nat) (case: SyntheticTactic): CoreM TacticResult :=
   runTermElabM do
     state.restoreElabM
-    state.execute goalId $ match case with
+    state.execute goalId $ match tacticExecute with
       | .congruenceArg => Tactic.congruenceArg
       | .congruenceFun => Tactic.congruenceFun
       | .congruence => Tactic.congruence

Pantograph/Serial.lean

@@ -4,10 +4,10 @@ This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
 using `Scope`s.
 -/
 import Lean
-import Pantograph.Condensed
 import Pantograph.Expr
-import Pantograph.Goal
+
 import Pantograph.Protocol
+import Pantograph.Goal
 
 open Lean
 
@@ -201,57 +201,8 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
     dependentMVars?,
   }
 
-@[export pantograph_to_condensed_goal]
-def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
-  let options: Protocol.Options := {}
-  let ppAuxDecls       := options.printAuxDecls
-  let ppImplDetailHyps := options.printImplementationDetailHyps
-  let mvarDecl ← mvarId.getDecl
-  let lctx     := mvarDecl.lctx
-  let lctx     := lctx.sanitizeNames.run' { options := (← getOptions) }
-  Meta.withLCtx lctx mvarDecl.localInstances do
-    let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
-      match localDecl with
-      | .cdecl _ fvarId userName type _ _ =>
-        let type ← instantiate type
-        return { fvarId, userName, type }
-      | .ldecl _ fvarId userName type value _ _ => do
-        let userName := userName.simpMacroScopes
-        let type ← instantiate type
-        let value ← instantiate value
-        return { fvarId, userName, type, value? := .some value }
-    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
-      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
-        !ppImplDetailHyps && localDecl.isImplementationDetail
-      if skip then
-        return acc
-      else
-        let var ← ppVar localDecl
-        return var::acc
-    return {
-        mvarId,
-        userName := mvarDecl.userName,
-        context := vars.reverse.toArray,
-        target := ← instantiate mvarDecl.type
-    }
-  where
-  instantiate := instantiateAll
-
-@[export pantograph_goal_state_to_condensed]
-protected def GoalState.toCondensed (state: GoalState):
-    CoreM (Array Condensed.Goal):= do
-  let metaM := do
-    let goals := state.goals.toArray
-    goals.mapM fun goal => do
-      match state.mctx.findDecl? goal with
-      | .some _ =>
-        let serializedGoal ← toCondensedGoal goal
-        pure serializedGoal
-      | .none => throwError s!"Metavariable does not exist in context {goal.name}"
-  metaM.run' (s := state.savedState.term.meta.meta)
-
 /-- Adapted from ppGoal -/
-def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
+def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
       : MetaM Protocol.Goal := do
   -- Options for printing; See Meta.ppGoal for details
   let showLetValues  := true
@@ -263,6 +214,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
     let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
       match localDecl with
       | .cdecl _ fvarId userName _ _ _ =>
+        let userName := userName.simpMacroScopes
         return {
           name := ofName fvarId.name,
           userName:= ofName userName.simpMacroScopes,
@@ -359,7 +311,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
       let pref := if goalState.newMVars.contains mvarId then "~" else " "
       printMVar pref mvarId decl
   )
-  pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
+  pure $ result ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
   where
     printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
       let resultFVars: List String ←
@@ -385,7 +337,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
               else pure $ value
             pure s!"\n := {← Meta.ppExpr value}"
           else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
-            pure s!"\n ::= {mvarIdPending.name}"
+            pure s!"\n := $ {mvarIdPending.name}"
           else
             pure ""
         else

Pantograph/Tactic/Prograde.lean

@@ -5,7 +5,7 @@ open Lean
 
 namespace Pantograph.Tactic
 
-def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
+def tacticEval (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
   let nextGoals ← goal.withContext do
     let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
@@ -19,29 +19,4 @@ def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
     pure [mvarUpstream.mvarId!]
   Elab.Tactic.setGoals nextGoals
 
-def «have» (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
-  let goal ← Elab.Tactic.getMainGoal
-  let nextGoals: List MVarId ← goal.withContext do
-    let type ← Elab.Term.elabType (stx := type)
-    let lctx ← MonadLCtx.getLCtx
-
-    -- The branch goal inherits the same context, but with a different type
-    let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
-
-    -- Create the context for the `upstream` goal
-    let fvarId ← mkFreshFVarId
-    let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
-    let fvar   := mkFVar fvarId
-    let mvarUpstream ←
-      withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
-        Meta.withNewLocalInstances #[fvar] 0 do
-          let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
-            (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
-          --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
-          goal.assign mvarUpstream
-          pure mvarUpstream
-
-    pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
-  Elab.Tactic.setGoals nextGoals
-
 end Pantograph.Tactic

Test/Common.lean

@@ -1,7 +1,6 @@
 import Pantograph.Goal
 import Pantograph.Library
 import Pantograph.Protocol
-import Pantograph.Condensed
 import Lean
 import LSpec
 
@@ -9,19 +8,12 @@ open Lean
 
 namespace Pantograph
 
-deriving instance Repr for Expr
--- Use strict equality check for expressions
-instance : BEq Expr := ⟨Expr.equal⟩
-
-def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
-
 -- Auxiliary functions
 namespace Protocol
 def Goal.devolatilizeVars (goal: Goal): Goal :=
   {
     goal with
     vars := goal.vars.map removeInternalAux,
-
   }
   where removeInternalAux (v: Variable): Variable :=
     {
@@ -44,24 +36,6 @@ deriving instance DecidableEq, Repr for InteractionError
 deriving instance DecidableEq, Repr for Option
 end Protocol
 
-namespace Condensed
-
-deriving instance BEq, Repr for LocalDecl
-deriving instance BEq, Repr for Goal
-
-protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
-  {
-    decl with fvarId := { name := .anonymous }
-  }
-protected def Goal.devolatilize (goal: Goal): Goal :=
-  {
-    goal with
-    mvarId := { name := .anonymous },
-    context := goal.context.map LocalDecl.devolatilize
-  }
-
-end Condensed
-
 def TacticResult.toString : TacticResult → String
   | .success state => s!".success ({state.goals.length} goals)"
   | .failure messages =>

Test/Main.lean

@@ -52,7 +52,6 @@ def main (args: List String) := do
     ("Tactic/Congruence", Tactic.Congruence.suite env_default),
     ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
     ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
-    ("Tactic/Prograde", Tactic.Prograde.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

@@ -1,4 +1,3 @@
 import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse
-import Test.Tactic.Prograde

Test/Tactic/Congruence.lean

@@ -7,34 +7,6 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.Congruence
 
-def test_congr_arg_list (env: Environment): IO LSpec.TestSeq :=
-  let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
-  runMetaMSeq env do
-    let expr ← parseSentence expr
-    Meta.lambdaTelescope expr $ λ _ body => do
-      let mut tests := LSpec.TestSeq.done
-      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let (newGoals, test) ← runTermElabMInMeta do
-        let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
-        let test := LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-          [
-            (`α, "Sort ?u.30"),
-            (`a₁, "?α"),
-            (`a₂, "?α"),
-            (`f, "?α → List α"),
-            (`h, "?a₁ = ?a₂"),
-            (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
-          ])
-        return (newGoals, test)
-      tests := tests ++ test
-      let f := newGoals.get! 3
-      let h := newGoals.get! 4
-      let c := newGoals.get! 5
-      let results ← f.apply (← parseSentence "List.reverse")
-      tests := tests ++ (LSpec.check "apply" (results.length = 0))
-      tests := tests ++ (LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂"))
-      tests := tests ++ (LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)"))
-      return tests
 def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
   runMetaMSeq env do
@@ -100,7 +72,6 @@ def test_congr (env: Environment): IO LSpec.TestSeq :=
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("congrArg List.reverse", test_congr_arg_list env),
     ("congrArg", test_congr_arg env),
     ("congrFun", test_congr_fun env),
     ("congr", test_congr env),

Test/Tactic/Prograde.lean

@@ -1,63 +0,0 @@
-import LSpec
-import Lean
-import Test.Common
-
-open Lean
-open Pantograph
-
-namespace Pantograph.Test.Tactic.Prograde
-
-def test_eval (env: Environment): IO LSpec.TestSeq :=
-  let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
-  runMetaMSeq env do
-    let expr ← parseSentence expr
-    Meta.forallTelescope expr $ λ _ body => do
-      let e ← match Parser.runParserCategory
-        (env := ← MonadEnv.getEnv)
-        (catName := `term)
-        (input := "Or.inl h")
-        (fileName := filename) with
-        | .ok syn => pure syn
-        | .error error => throwError "Failed to parse: {error}"
-      let mut tests := LSpec.TestSeq.done
-      -- Apply the tactic
-      let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let target: Expr := mkAnd
-        (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
-        (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
-      let h := .fvar ⟨uniq 8⟩
-      let test := LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == {
-        context := #[
-          { userName := `p, type := .sort 0 },
-          { userName := `q, type := .sort 0 },
-          { userName := `h, type := h}
-        ],
-        target,
-      })
-      tests := tests ++ test
-      let tactic := Tactic.evaluate `h2 e
-      let m := .mvar ⟨uniq 13⟩
-      let test ← runTermElabMInMeta do
-        let [goal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number"
-        pure $ LSpec.test "goals after" ((← toCondensedGoal goal).devolatilize == {
-        context := #[
-          { userName := `p, type := .sort 0 },
-          { userName := `q, type := .sort 0 },
-          { userName := `h, type := h},
-          {
-            userName := `h2,
-            type := mkOr h m,
-            value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩)
-          }
-        ],
-        target,
-      })
-      tests := tests ++ test
-      return tests
-
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("eval", test_eval env),
-  ]
-
-end Pantograph.Test.Tactic.Prograde