From ffbea41f627741e70e2b1d01ac8663b9acd12777 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 25 Jun 2024 15:13:58 -0400
Subject: [PATCH 01/26] feat: Condensed interface

---
 Pantograph/Condensed.lean | 42 ++++++++++++++++++++++++++++++
 Pantograph/Serial.lean    | 54 ++++++++++++++++++++++++++++++++++++---
 Test/Common.lean          | 11 ++++++++
 3 files changed, 104 insertions(+), 3 deletions(-)
 create mode 100644 Pantograph/Condensed.lean

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
new file mode 100644
index 0000000..57a8517
--- /dev/null
+++ b/Pantograph/Condensed.lean
@@ -0,0 +1,42 @@
+/- 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
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index e729bee..2cdf3d6 100644
--- a/Pantograph/Serial.lean
+++ b/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.Protocol
 import Pantograph.Goal
+import Pantograph.Protocol
 
 open Lean
 
@@ -201,6 +201,55 @@ 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)
       : MetaM Protocol.Goal := do
@@ -214,7 +263,6 @@ 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,
diff --git a/Test/Common.lean b/Test/Common.lean
index c656309..e4e1d4c 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -8,6 +8,17 @@ open Lean
 
 namespace Pantograph
 
+deriving instance Repr for Expr
+-- Use strict equality check for expressions
+--instance : BEq Expr := ⟨Expr.equal⟩
+instance (priority := 80) (x y : Expr) : LSpec.Testable (x.equal y) :=
+  if h : Expr.equal x y then
+    .isTrue h
+  else
+    .isFalse h $ s!"Expected to be equalaaa: '{x.dbgToString}' and '{y.dbgToString}'"
+
+def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
+
 -- Auxiliary functions
 namespace Protocol
 def Goal.devolatilizeVars (goal: Goal): Goal :=

From 8e78718447456d20b5c54e36384223ffad577bc3 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 25 Jun 2024 15:54:55 -0400
Subject: [PATCH 02/26] feat: Extract MetaM context and state from goal

---
 Pantograph/Goal.lean | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 46888e7..2723c4f 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -63,9 +63,16 @@ 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
-  let metaM := mvarId.withContext m
-  metaM.run' (← read) state.savedState.term.meta.meta
+  mvarId.withContext m |>.run' (← read) state.metaState
 
 protected def GoalState.withParentContext (state: GoalState) (m: MetaM α): MetaM α := do
   state.withContext state.parentMVar?.get! m
@@ -82,6 +89,7 @@ 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

From 193d94e7986fef4779f5ce171616a1bc3ad0d068 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 15 Jul 2024 11:42:02 -0700
Subject: [PATCH 03/26] feat: Expression creation and pretty printing

---
 Pantograph/Condensed.lean | 7 +++++++
 Pantograph/Library.lean   | 7 ++++---
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index 57a8517..f6f4cdb 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -17,6 +17,13 @@ def nameToStr (s: String) : Name := s.toName
 @[export pantograph_name_is_inaccessible]
 def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName
 
+@[export pantograph_mk_app_meta_m]
+def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs
+
+@[export pantograph_pp_expr]
+def ppExpr (e: Expr) := Meta.ppExpr e
+
+
 -- Mirrors Lean's LocalDecl
 structure LocalDecl where
   -- Default value is for testing
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 8036103..eb34614 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -78,9 +78,10 @@ def createCoreState (imports: Array String): IO Core.State := do
     (trustLevel := 1)
   return { env := env }
 
-@[export pantograph_create_meta_context]
-def createMetaContext: IO Lean.Meta.Context := do
-  return {}
+@[export pantograph_meta_context]
+def metaContext: Lean.Meta.Context := {}
+@[export pantograph_meta_state]
+def metaState: Lean.Meta.State := {}
 
 @[export pantograph_env_catalog_m]
 def envCatalog: CoreM Protocol.EnvCatalogResult :=

From 94c7b021f77c02376ad0219cdef97b1a06bc0d1b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 15 Jul 2024 12:22:47 -0700
Subject: [PATCH 04/26] fix: Signature of ppExpr

---
 Pantograph/Condensed.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index f6f4cdb..8b3de4f 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -20,8 +20,8 @@ def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName
 @[export pantograph_mk_app_meta_m]
 def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs
 
-@[export pantograph_pp_expr]
-def ppExpr (e: Expr) := Meta.ppExpr e
+@[export pantograph_pp_expr_meta_m]
+def ppExpr (e: Expr): MetaM String := toString<$> Meta.ppExpr e
 
 
 -- Mirrors Lean's LocalDecl

From eb5ee8c57c395f60c6c7108e629ac248a3625c89 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 22 Jul 2024 17:34:14 -0700
Subject: [PATCH 05/26] feat: Expose TermElab context and state

---
 Pantograph/Condensed.lean | 20 ++++++++++++++++----
 Pantograph/Library.lean   |  7 ++-----
 2 files changed, 18 insertions(+), 9 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index 8b3de4f..a1688f1 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -13,15 +13,15 @@ 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
+def nameToStr (s: Name) : String := s.toString
 @[export pantograph_name_is_inaccessible]
 def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName
 
-@[export pantograph_mk_app_meta_m]
+@[export pantograph_mk_app_m]
 def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs
 
-@[export pantograph_pp_expr_meta_m]
-def ppExpr (e: Expr): MetaM String := toString<$> Meta.ppExpr e
+@[export pantograph_pp_expr_m]
+def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e
 
 
 -- Mirrors Lean's LocalDecl
@@ -44,6 +44,18 @@ structure Goal where
 def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
 
 
+-- Functions for creating contexts and states
+@[export pantograph_meta_context]
+def metaContext: Meta.Context := {}
+@[export pantograph_meta_state]
+def metaState: Meta.State := {}
+@[export pantograph_elab_context]
+def elabContext: Meta.Context := {}
+@[export pantograph_elab_state]
+def elabState (levelNames: Array Name): Elab.Term.State := {
+    levelNames := levelNames.toList,
+  }
+
 
 
 end Pantograph.Condensed
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index eb34614..3bc3cc1 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -78,11 +78,6 @@ def createCoreState (imports: Array String): IO Core.State := do
     (trustLevel := 1)
   return { env := env }
 
-@[export pantograph_meta_context]
-def metaContext: Lean.Meta.Context := {}
-@[export pantograph_meta_state]
-def metaState: Lean.Meta.State := {}
-
 @[export pantograph_env_catalog_m]
 def envCatalog: CoreM Protocol.EnvCatalogResult :=
   Environment.catalog ({}: Protocol.EnvCatalog)
@@ -99,6 +94,7 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
     CoreM (Protocol.CR Protocol.EnvAddResult) :=
   Environment.addDecl { name, type, value, isTheorem }
 
+@[export pantograph_parse_elab_type_m]
 def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
   let env ← MonadEnv.getEnv
   let syn ← match parseTerm env type with
@@ -109,6 +105,7 @@ def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
   | .ok expr => return .ok (← instantiateMVars expr)
 
 /-- This must be a TermElabM since the parsed expr contains extra information -/
+@[export pantograph_parse_elab_expr_m]
 def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do
   let env ← MonadEnv.getEnv
   let expectedType? ← match ← expectedType?.mapM parseElabType with

From 431ca4e481fb1856d36ed17f322419ab59ed8e25 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 22 Jul 2024 17:57:01 -0700
Subject: [PATCH 06/26] fix: Move elab context to condensed

---
 Pantograph/Condensed.lean | 5 +++--
 Pantograph/Library.lean   | 6 ++----
 Test/Common.lean          | 2 +-
 Test/Metavar.lean         | 2 +-
 Test/Proofs.lean          | 2 +-
 Test/Serial.lean          | 4 ++--
 6 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index a1688f1..ac41133 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -50,12 +50,13 @@ def metaContext: Meta.Context := {}
 @[export pantograph_meta_state]
 def metaState: Meta.State := {}
 @[export pantograph_elab_context]
-def elabContext: Meta.Context := {}
+def elabContext: Elab.Term.Context := {
+    errToSorry := false
+  }
 @[export pantograph_elab_state]
 def elabState (levelNames: Array Name): Elab.Term.State := {
     levelNames := levelNames.toList,
   }
 
 
-
 end Pantograph.Condensed
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 3bc3cc1..2f37cfa 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -1,3 +1,4 @@
+import Pantograph.Condensed
 import Pantograph.Environment
 import Pantograph.Goal
 import Pantograph.Protocol
@@ -38,13 +39,10 @@ open Lean
 
 namespace Pantograph
 
-def defaultTermElabMContext: Elab.Term.Context := {
-    errToSorry := false
-  }
 def runMetaM { α } (metaM: MetaM α): CoreM α :=
   metaM.run'
 def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
-  termElabM.run' (ctx := defaultTermElabMContext) |>.run'
+  termElabM.run' (ctx := Condensed.elabContext) |>.run'
 
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
 
diff --git a/Test/Common.lean b/Test/Common.lean
index e4e1d4c..4b17736 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -73,7 +73,7 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
 def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
   runCoreMSeq env metaM.run'
 def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
-  termElabM.run' (ctx := Pantograph.defaultTermElabMContext)
+  termElabM.run' (ctx := Pantograph.Condensed.elabContext)
 
 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
 
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 0818881..4ac8454 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -67,7 +67,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
   let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
 
   let coreContext: Lean.Core.Context ← createCoreContext #[]
-  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
+  let metaM := termElabM.run' (ctx := Condensed.elabContext)
   let coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 9c45138..51e869d 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -76,7 +76,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
   let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
 
   let coreContext: Lean.Core.Context ← createCoreContext #[]
-  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
+  let metaM := termElabM.run' (ctx := Condensed.elabContext)
   let coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
diff --git a/Test/Serial.lean b/Test/Serial.lean
index 2d2b9d1..1c00501 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -64,7 +64,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
         | .ok expr => pure expr
         | .error e => return elabFailure e
       return LSpec.check source ((← serializeExpressionSexp expr) = target)
-    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultTermElabMContext)
+    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := Condensed.elabContext)
     return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
     LSpec.TestSeq.done
 
@@ -85,7 +85,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
     let testCaseName := target.take 10
     let test := LSpec.check   testCaseName ((← serializeExpressionSexp expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-  runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
+  runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
 
 -- Instance parsing
 def test_instance (env: Environment): IO LSpec.TestSeq :=

From 3b415e8dc12485f7b2b9fa6f54329f6ad598d48f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 23 Jul 2024 05:16:46 -0700
Subject: [PATCH 07/26] chore: Rename exports

---
 Pantograph/Expr.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index 63331af..8ef0aa6 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -98,7 +98,7 @@ Convert an expression to an equiavlent form with
 2. No aux lemmas
 3. No assigned mvars
  -/
-@[export pantograph_instantiate_all_meta_m]
+@[export pantograph_instantiate_all_m]
 def instantiateAll (e: Expr): MetaM Expr := do
   let e ← instantiateDelayedMVars e
   let e ← unfoldAuxLemmas e
@@ -111,7 +111,7 @@ structure DelayedMVarInvocation where
   tail: Array Expr
 
 -- The pending mvar of any delayed assigned mvar must not be assigned in any way.
-@[export pantograph_to_delayed_mvar_invocation_meta_m]
+@[export pantograph_to_delayed_mvar_invocation_m]
 def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
   let .mvar mvarId := e.getAppFn | return .none
   let .some decl ← getDelayedMVarAssignment? mvarId | return .none

From 2682ce5b7b5a7e494d166b20b17852e88bea448a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 23 Jul 2024 11:57:12 -0700
Subject: [PATCH 08/26] refactor: Move condensed functions to condensed

---
 Pantograph/Condensed.lean | 58 +++++++++++++++++++++++++++++++++++++--
 Pantograph/Serial.lean    | 48 --------------------------------
 2 files changed, 56 insertions(+), 50 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index ac41133..90fc050 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -1,9 +1,13 @@
 /- structures for FFI based interface -/
 import Lean
+import Pantograph.Goal
+import Pantograph.Expr
+import Pantograph.Protocol
 
 open Lean
 
-namespace Pantograph.Condensed
+namespace Pantograph
+namespace Condensed
 
 /-
 These two functions are for user defiend names. For internal names such as
@@ -58,5 +62,55 @@ def elabState (levelNames: Array Name): Elab.Term.State := {
     levelNames := levelNames.toList,
   }
 
+end Condensed
 
-end Pantograph.Condensed
+@[export pantograph_to_condensed_goal_m]
+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_m]
+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)
+
+end Pantograph
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 2cdf3d6..87353e2 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -201,54 +201,6 @@ 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)

From bf941cd6862b2658146dbdde9db8079e7e08973e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 27 Jul 2024 17:39:51 -0700
Subject: [PATCH 09/26] feat: Expose parent and root expr functions

---
 Pantograph/Goal.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index c441ad9..398386e 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -136,6 +136,7 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
   else
     target.resume (goals := branch.goals)
 
+@[export pantograph_goal_state_root_expr]
 protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
   let expr ← goalState.mctx.eAssignment.find? goalState.root
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
@@ -146,12 +147,14 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
   else
     assert! goalState.goals.isEmpty
     return expr
+@[export pantograph_goal_state_parent_expr]
 protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
   let parent ← goalState.parentMVar?
   let expr := goalState.mctx.eAssignment.find! parent
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
   return expr
-protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do
+@[export pantograph_goal_state_get_mvar_e_assignment]
+protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId): Option Expr := do
   let expr ← goalState.mctx.eAssignment.find? mvar
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
   return expr

From 9db546349925730b445b6cf66fff29cc9dfcc52c Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 27 Jul 2024 18:20:34 -0700
Subject: [PATCH 10/26] feat: Export `GoalState.resume`

---
 Pantograph/Goal.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 398386e..b44e8d3 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -108,6 +108,7 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
 /--
 Brings into scope a list of goals
 -/
+@[export pantograph_goal_state_resume]
 protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
   if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
     let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)

From 4c81f226d1953aa93c131d5161b397a037f920a2 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 28 Jul 2024 13:46:14 -0700
Subject: [PATCH 11/26] feat: Expose environment functions

---
 Pantograph/Condensed.lean   |  4 +++-
 Pantograph/Environment.lean | 22 +++++++++++++++++++---
 Pantograph/Expr.lean        |  1 +
 3 files changed, 23 insertions(+), 4 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index 90fc050..8b5c313 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -19,13 +19,15 @@ def strToName (s: String) : Name := s.toName
 @[export pantograph_name_to_str]
 def nameToStr (s: Name) : String := s.toString
 @[export pantograph_name_is_inaccessible]
-def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName
+def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroScopes
 
 @[export pantograph_mk_app_m]
 def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs
 
 @[export pantograph_pp_expr_m]
 def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e
+@[export pantograph_get_used_constants]
+def getUsedConstants (e: Expr) := e.getUsedConstants
 
 
 -- Mirrors Lean's LocalDecl
diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index 6d91abb..a9b2934 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -7,15 +7,31 @@ open Pantograph
 
 namespace Pantograph.Environment
 
-def isNameInternal (n: Lean.Name): Bool :=
+@[export pantograph_is_name_internal]
+def isNameInternal (n: Name): Bool :=
   -- Returns true if the name is an implementation detail which should not be shown to the user.
   isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes
   where
-  isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
+  isLeanSymbol (name: Name): Bool := match name.getRoot with
     | .str _ name => name == "Lean"
     | _ => true
 
-def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
+/-- Catalog all the non-internal names -/
+@[export pantograph_environment_catalog]
+def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ =>
+  match isNameInternal name with
+  | true => acc.push name
+  | false => acc)
+
+@[export pantograph_environment_module_of_name]
+def module_of_name (env: Environment) (name: Name): Option Name := do
+  let moduleId ←  env.getModuleIdxFor? name
+  return env.allImportedModuleNames.get! moduleId.toNat
+
+@[export pantograph_constant_info_is_unsafe_or_partial]
+def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial
+
+def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
   let pref := match info with
   | .axiomInfo  _ => "a"
   | .defnInfo   _ => "d"
diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index 8ef0aa6..9d8f70c 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -7,6 +7,7 @@ namespace Pantograph
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
+@[export pantograph_unfold_aux_lemmas]
 def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 

From 29f437f859e3c7fad5a48fdce1fddc106991e586 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 28 Jul 2024 13:58:20 -0700
Subject: [PATCH 12/26] feat: Export GoalState.create

---
 Pantograph/Goal.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index b44e8d3..6dbe525 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -33,6 +33,7 @@ structure GoalState where
   -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
   calcPrevRhs?: Option Expr := .none
 
+@[export pantograph_goal_state_create_m]
 protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
   -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
   -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070

From 7b5567d784397c9d2a33b9464b5a1dd75fceb34a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 28 Jul 2024 14:19:47 -0700
Subject: [PATCH 13/26] fix: Name internal order

---
 Pantograph/Environment.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index a9b2934..d89486c 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -20,8 +20,8 @@ def isNameInternal (n: Name): Bool :=
 @[export pantograph_environment_catalog]
 def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ =>
   match isNameInternal name with
-  | true => acc.push name
-  | false => acc)
+  | false => acc.push name
+  | true => acc)
 
 @[export pantograph_environment_module_of_name]
 def module_of_name (env: Environment) (name: Name): Option Name := do

From 1c9a411d4d89db0bfc38cee2e2d0ff5f61a8c61b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 29 Jul 2024 18:39:22 -0700
Subject: [PATCH 14/26] feat: Export constant info type/value

---
 Pantograph/Environment.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index d89486c..37faf72 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -16,10 +16,10 @@ def isNameInternal (n: Name): Bool :=
     | .str _ name => name == "Lean"
     | _ => true
 
-/-- Catalog all the non-internal names -/
+/-- Catalog all the non-internal and safe names -/
 @[export pantograph_environment_catalog]
-def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ =>
-  match isNameInternal name with
+def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name info =>
+  match isNameInternal name || info.isUnsafe with
   | false => acc.push name
   | true => acc)
 
@@ -31,6 +31,11 @@ def module_of_name (env: Environment) (name: Name): Option Name := do
 @[export pantograph_constant_info_is_unsafe_or_partial]
 def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial
 
+@[export pantograph_constant_info_type]
+def constantInfoType (info: ConstantInfo): CoreM Expr := unfoldAuxLemmas info.type
+@[export pantograph_constant_info_value]
+def constantInfoValue (info: ConstantInfo): CoreM (Option Expr) := info.value?.mapM unfoldAuxLemmas
+
 def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
   let pref := match info with
   | .axiomInfo  _ => "a"

From 3ca52517abe07ecd1c2036eeba4e2ba762299f9f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 30 Jul 2024 13:30:41 -0700
Subject: [PATCH 15/26] feat: Refactor out projToApp

---
 Pantograph/Expr.lean   | 20 ++++++++++++++++++++
 Pantograph/Serial.lean | 13 +++++--------
 2 files changed, 25 insertions(+), 8 deletions(-)

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index 9d8f70c..cbee9a5 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -4,6 +4,26 @@ open Lean
 
 namespace Pantograph
 
+structure ProjectionApplication where
+  projector: Name
+  numParams: Nat
+  inner: Expr
+
+@[export pantograph_expr_proj_to_app]
+def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
+  let (typeName, idx, inner) := match e with
+    | .proj typeName idx inner => (typeName, idx, inner)
+    | _ => panic! "Argument must be proj"
+  let ctor := getStructureCtor env typeName
+  let fieldName := getStructureFields env typeName |>.get! idx
+  let projector := getProjFnForField? env typeName fieldName |>.get!
+  {
+    projector,
+    numParams := ctor.numParams,
+    inner,
+  }
+
+
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 87353e2..21bffce 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -168,15 +168,12 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
       -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
       -- It may become necessary to incorporate the metadata.
       self inner
-    | .proj typeName idx inner => do
+    | .proj _ _ _ => do
       let env ← getEnv
-      let ctor := getStructureCtor env typeName
-      let fieldName := getStructureFields env typeName |>.get! idx
-      let projectorName := getProjFnForField? env typeName fieldName |>.get!
-
-      let autos := String.intercalate " " (List.replicate ctor.numParams "_")
-      let inner ← self inner
-      pure s!"((:c {projectorName}) {autos} {inner})"
+      let projApp := exprProjToApp env e
+      let autos := String.intercalate " " (List.replicate projApp.numParams "_")
+      let inner ← self projApp.inner
+      pure s!"((:c {projApp.projector}) {autos} {inner})"
   -- Elides all unhygenic names
   binderInfoSexp : Lean.BinderInfo → String
     | .default => ""

From caa463f41010326d1f7c213ae2614b9fabacb73d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 30 Jul 2024 17:02:41 -0700
Subject: [PATCH 16/26] feat: Export GoalState.goalsArray

---
 Pantograph/Expr.lean    |  1 -
 Pantograph/Goal.lean    |  2 ++
 Pantograph/Library.lean | 11 -----------
 3 files changed, 2 insertions(+), 12 deletions(-)

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index cbee9a5..f989575 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -23,7 +23,6 @@ def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
     inner,
   }
 
-
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 6dbe525..26a8da1 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -54,6 +54,8 @@ protected def GoalState.isConv (state: GoalState): Bool :=
   state.convMVar?.isSome
 protected def GoalState.goals (state: GoalState): List MVarId :=
   state.savedState.tactic.goals
+@[export pantograph_goal_state_goals]
+protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray
 protected def GoalState.mctx (state: GoalState): MetavarContext :=
   state.savedState.term.meta.meta.mctx
 protected def GoalState.env (state: GoalState): Environment :=
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 2f37cfa..5aa8f35 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -76,17 +76,6 @@ def createCoreState (imports: Array String): IO Core.State := do
     (trustLevel := 1)
   return { env := env }
 
-@[export pantograph_env_catalog_m]
-def envCatalog: CoreM Protocol.EnvCatalogResult :=
-  Environment.catalog ({}: Protocol.EnvCatalog)
-
-@[export pantograph_env_inspect_m]
-def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
-    CoreM (Protocol.CR Protocol.EnvInspectResult) :=
-  Environment.inspect ({
-    name, value? := .some value, dependency?:= .some dependency
-  }: Protocol.EnvInspect) options
-
 @[export pantograph_env_add_m]
 def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
     CoreM (Protocol.CR Protocol.EnvAddResult) :=

From abef7a6f0d55de552c3c7297d25ece8121ee931d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 31 Jul 2024 00:00:21 -0700
Subject: [PATCH 17/26] feat: Export fvar names function

---
 Pantograph/Goal.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 26a8da1..0e87a12 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -69,6 +69,11 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O
 protected def GoalState.metaState (state: GoalState): Meta.State :=
   state.savedState.term.meta.meta
 
+@[export pantograph_goal_state_fvar_names_of_goal]
+protected def GoalState.fvarNamesOfGoal (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do
+  let mvarDecl ← state.mctx.findDecl? mvarId
+  return mvarDecl.lctx.getFVarIds
+
 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
   mvarId.withContext m |>.run' (← read) state.metaState
 

From 651afa75f4cb8cbd10c77247e055177c5adeed56 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 2 Aug 2024 19:49:11 -0700
Subject: [PATCH 18/26] feat: Filter in `visibleFVarsOfMVar`

---
 Pantograph/Condensed.lean | 14 +++++++++++---
 Pantograph/Goal.lean      | 10 +++++++---
 2 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index 8b5c313..1db3c62 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -66,11 +66,19 @@ def elabState (levelNames: Array Name): Elab.Term.State := {
 
 end Condensed
 
+-- Get the list of visible (by default) free variables from a goal
+@[export pantograph_visible_fvars_of_mvar]
+protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
+  let mvarDecl ← mctx.findDecl? mvarId
+  let lctx := mvarDecl.lctx
+  return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
+    | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
+    | none      => r
+
 @[export pantograph_to_condensed_goal_m]
 def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
-  let options : Protocol.Options := {}
-  let ppAuxDecls       := options.printAuxDecls
-  let ppImplDetailHyps := options.printImplementationDetailHyps
+  let ppAuxDecls     := Meta.pp.auxDecls.get (← getOptions)
+  let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
   let mvarDecl ← mvarId.getDecl
   let lctx     := mvarDecl.lctx
   let lctx     := lctx.sanitizeNames.run' { options := (← getOptions) }
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 0e87a12..ccb7a3d 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -69,10 +69,14 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O
 protected def GoalState.metaState (state: GoalState): Meta.State :=
   state.savedState.term.meta.meta
 
-@[export pantograph_goal_state_fvar_names_of_goal]
-protected def GoalState.fvarNamesOfGoal (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do
+-- Get the list of visible free variables from a goal
+@[export pantograph_goal_state_visible_fvars]
+protected def GoalState.visibleFVars (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do
   let mvarDecl ← state.mctx.findDecl? mvarId
-  return mvarDecl.lctx.getFVarIds
+  let lctx := mvarDecl.lctx
+  return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
+    | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
+    | none      => r
 
 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
   mvarId.withContext m |>.run' (← read) state.metaState

From 2c08ef1e23a3429cefb5aacad19819a92768a847 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 2 Aug 2024 19:53:19 -0700
Subject: [PATCH 19/26] refactor: Remove old `visibleFVars` interface

---
 Pantograph/Goal.lean | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index ccb7a3d..26a8da1 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -69,15 +69,6 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O
 protected def GoalState.metaState (state: GoalState): Meta.State :=
   state.savedState.term.meta.meta
 
--- Get the list of visible free variables from a goal
-@[export pantograph_goal_state_visible_fvars]
-protected def GoalState.visibleFVars (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do
-  let mvarDecl ← state.mctx.findDecl? mvarId
-  let lctx := mvarDecl.lctx
-  return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
-    | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
-    | none      => r
-
 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
   mvarId.withContext m |>.run' (← read) state.metaState
 

From c0e2a592ea819389bd5a39d289aabdd3d7a26a75 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 2 Aug 2024 21:44:46 -0700
Subject: [PATCH 20/26] feat: Expose `mkAppM'`

---
 Pantograph/Condensed.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index 1db3c62..fcd70a0 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -23,6 +23,8 @@ def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroSco
 
 @[export pantograph_mk_app_m]
 def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs
+@[export pantograph_mk_app_m_expr]
+def mkAppM' (f: Expr) (xs : Array Expr) : MetaM Expr := Meta.mkAppM' f xs
 
 @[export pantograph_pp_expr_m]
 def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e

From 394fb731375785d268184c640cd387f44d76dac4 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 2 Aug 2024 22:00:27 -0700
Subject: [PATCH 21/26] feat: Add direct expression to string

---
 Pantograph/Condensed.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index fcd70a0..9c20f32 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -23,9 +23,11 @@ def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroSco
 
 @[export pantograph_mk_app_m]
 def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs
-@[export pantograph_mk_app_m_expr]
+@[export pantograph_mk_app_expr_m]
 def mkAppM' (f: Expr) (xs : Array Expr) : MetaM Expr := Meta.mkAppM' f xs
 
+@[export pantograph_expr_to_string]
+def exprToString (e: Expr): String := toString e
 @[export pantograph_pp_expr_m]
 def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e
 @[export pantograph_get_used_constants]

From c9ee31bbfdd215e5ceba960218c8344afd46954e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 2 Aug 2024 22:33:03 -0700
Subject: [PATCH 22/26] feat: Export `mkFun`

---
 Pantograph/Condensed.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index 9c20f32..8696523 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -25,6 +25,14 @@ def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroSco
 def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs
 @[export pantograph_mk_app_expr_m]
 def mkAppM' (f: Expr) (xs : Array Expr) : MetaM Expr := Meta.mkAppM' f xs
+-- Copies same function in `Meta/AppBuilder.lean`
+@[export pantograph_mk_fun_m]
+def mkFun (constName : Name) : MetaM (Expr × Expr) := do
+  let cinfo ← getConstInfo constName
+  let us ← cinfo.levelParams.mapM fun _ => Meta.mkFreshLevelMVar
+  let f := mkConst constName us
+  let fType ← Meta.instantiateTypeLevelParams cinfo us
+  return (f, fType)
 
 @[export pantograph_expr_to_string]
 def exprToString (e: Expr): String := toString e

From 64269868d518b1211b724a46dc080d6f2f5a4a44 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 4 Aug 2024 17:32:20 -0700
Subject: [PATCH 23/26] feat: Expose project and leanPkgs in flake

---
 flake.nix | 1 +
 1 file changed, 1 insertion(+)

diff --git a/flake.nix b/flake.nix
index b96d5e2..54a139f 100644
--- a/flake.nix
+++ b/flake.nix
@@ -63,6 +63,7 @@
       packages = {
         inherit (leanPkgs) lean lean-all;
         inherit (project) sharedLib executable;
+        inherit project leanPkgs;
         default = project.executable;
       };
       checks = {

From caac70f0cfedca3964f65d2dbd04a8370c5dd97f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 4 Aug 2024 17:52:36 -0700
Subject: [PATCH 24/26] feat: Move non package outputs to dependencies

---
 flake.nix | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/flake.nix b/flake.nix
index 54a139f..2b68c0c 100644
--- a/flake.nix
+++ b/flake.nix
@@ -63,9 +63,11 @@
       packages = {
         inherit (leanPkgs) lean lean-all;
         inherit (project) sharedLib executable;
-        inherit project leanPkgs;
         default = project.executable;
       };
+      dependencies = {
+        inherit project leanPkgs;
+      };
       checks = {
         test = pkgs.runCommand "test" {
           buildInputs = [ test.executable leanPkgs.lean-all ];

From 0bc7bc58565cceb839c41a11d207e4eeb64a845e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 14 Aug 2024 01:20:56 -0700
Subject: [PATCH 25/26] refactor: Remove export of Lean functions

If the user wishes to use Lean functions, they should add the bindings manually.
---
 Pantograph/Condensed.lean | 42 ---------------------------------------
 flake.nix                 |  4 +---
 2 files changed, 1 insertion(+), 45 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index 8696523..c47f882 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -9,39 +9,6 @@ open Lean
 namespace Pantograph
 namespace 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: Name) : String := s.toString
-@[export pantograph_name_is_inaccessible]
-def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroScopes
-
-@[export pantograph_mk_app_m]
-def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs
-@[export pantograph_mk_app_expr_m]
-def mkAppM' (f: Expr) (xs : Array Expr) : MetaM Expr := Meta.mkAppM' f xs
--- Copies same function in `Meta/AppBuilder.lean`
-@[export pantograph_mk_fun_m]
-def mkFun (constName : Name) : MetaM (Expr × Expr) := do
-  let cinfo ← getConstInfo constName
-  let us ← cinfo.levelParams.mapM fun _ => Meta.mkFreshLevelMVar
-  let f := mkConst constName us
-  let fType ← Meta.instantiateTypeLevelParams cinfo us
-  return (f, fType)
-
-@[export pantograph_expr_to_string]
-def exprToString (e: Expr): String := toString e
-@[export pantograph_pp_expr_m]
-def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e
-@[export pantograph_get_used_constants]
-def getUsedConstants (e: Expr) := e.getUsedConstants
-
-
 -- Mirrors Lean's LocalDecl
 structure LocalDecl where
   -- Default value is for testing
@@ -61,20 +28,11 @@ structure Goal where
 @[export pantograph_goal_is_lhs]
 def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
 
-
 -- Functions for creating contexts and states
-@[export pantograph_meta_context]
-def metaContext: Meta.Context := {}
-@[export pantograph_meta_state]
-def metaState: Meta.State := {}
 @[export pantograph_elab_context]
 def elabContext: Elab.Term.Context := {
     errToSorry := false
   }
-@[export pantograph_elab_state]
-def elabState (levelNames: Array Name): Elab.Term.State := {
-    levelNames := levelNames.toList,
-  }
 
 end Condensed
 
diff --git a/flake.nix b/flake.nix
index 2b68c0c..54a139f 100644
--- a/flake.nix
+++ b/flake.nix
@@ -63,10 +63,8 @@
       packages = {
         inherit (leanPkgs) lean lean-all;
         inherit (project) sharedLib executable;
-        default = project.executable;
-      };
-      dependencies = {
         inherit project leanPkgs;
+        default = project.executable;
       };
       checks = {
         test = pkgs.runCommand "test" {

From e943a4b065cc78c268fcd3ca31ff57d7d3e4b697 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 15 Aug 2024 22:39:40 -0700
Subject: [PATCH 26/26] refactor: Assign into its own tactic

---
 Pantograph/Goal.lean          | 68 ++++++-----------------------------
 Pantograph/Library.lean       | 19 ----------
 Pantograph/Serial.lean        |  6 ++--
 Pantograph/Tactic.lean        |  1 +
 Pantograph/Tactic/Assign.lean | 35 ++++++++++++++++++
 Test/Metavar.lean             |  4 +--
 6 files changed, 52 insertions(+), 81 deletions(-)
 create mode 100644 Pantograph/Tactic/Assign.lean

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 26a8da1..136379a 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -178,13 +178,14 @@ inductive TacticResult where
   -- The given action cannot be executed in the state
   | invalidAction (message: String)
 
-protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
-          Elab.TermElabM TacticResult := do
+/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
+protected def GoalState.executeTactic (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
+      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.execute
+  goal.checkNotAssigned `GoalState.executeTactic
   try
     let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
     if (← getThe Core.State).messages.hasErrors then
@@ -204,7 +205,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
-/-- Execute tactic on given state -/
+/-- Execute a string tactic on given state -/
 protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
     Elab.TermElabM TacticResult := do
   let tactic ← match Parser.runParserCategory
@@ -214,68 +215,19 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
     (fileName := filename) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  state.execute goalId $ Elab.Tactic.evalTactic tactic
-
-/-- Assumes elabM has already been restored. Assumes expr has already typechecked -/
-protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
-      Elab.TermElabM TacticResult := do
-  let goalType ← goal.getType
-  try
-    -- For some reason this is needed. One of the unit tests will fail if this isn't here
-    let error?: Option String ← goal.withContext do
-      let exprType ← Meta.inferType expr
-      if ← Meta.isDefEq goalType exprType then
-        pure .none
-      else do
-        return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}"
-    if let .some error := error? then
-      return .parseError error
-    goal.checkNotAssigned `GoalState.assign
-    goal.assign expr
-    if (← getThe Core.State).messages.hasErrors then
-      let messages := (← getThe Core.State).messages.toArray
-      let errors ← (messages.map (·.data)).mapM fun md => md.toString
-      return .failure errors
-    let prevMCtx := state.savedState.term.meta.meta.mctx
-    let nextMCtx ← getMCtx
-    -- Generate a list of mvarIds that exist in the parent state; Also test the
-    -- assertion that the types have not changed on any mvars.
-    let newMVars := newMVarSet prevMCtx nextMCtx
-    let nextGoals ← newMVars.toList.filterM (not <$> ·.isAssigned)
-    return .success {
-      root := state.root,
-      savedState := {
-        term := ← MonadBacktrack.saveState,
-        tactic := { goals := nextGoals }
-      },
-      newMVars,
-      parentMVar? := .some goal,
-      calcPrevRhs? := .none
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
+  state.executeTactic goalId $ Elab.Tactic.evalTactic tactic
 
 protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: 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.tryAssign
   let expr ← match Parser.runParserCategory
-    (env := state.env)
+    (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := expr)
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  let goalType ← goal.getType
-  try
-    let expr ← goal.withContext $
-      Elab.Term.elabTermAndSynthesize (stx := expr) (expectedType? := .some goalType)
-    state.assign goal expr
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
+  state.executeTactic goalId $ Tactic.evalAssign expr
 
 -- Specialized Tactics
 
@@ -535,7 +487,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.motivatedApply recursor)
+  state.executeTactic goalId (tacticM := Tactic.motivatedApply recursor)
 protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
@@ -546,6 +498,6 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: Strin
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.noConfuse recursor)
+  state.executeTactic goalId (tacticM := Tactic.noConfuse recursor)
 
 end Pantograph
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 5aa8f35..59197f6 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -154,9 +154,6 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.G
         state.withParentContext do
           serializeExpression options (← instantiateAll expr)),
     }
-@[export pantograph_goal_diag_m]
-def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : CoreM String :=
-  runMetaM $ state.diag diagOptions
 
 @[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult :=
@@ -189,20 +186,4 @@ 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
-  | congruenceArg
-  | congruenceFun
-  | congruence
-/-- Executes a synthetic tactic which has no arguments -/
-@[export pantograph_goal_synthetic_tactic_m]
-def goalSyntheticTactic (state: GoalState) (goalId: Nat) (case: SyntheticTactic): CoreM TacticResult :=
-  runTermElabM do
-    state.restoreElabM
-    state.execute goalId $ match case with
-      | .congruenceArg => Tactic.congruenceArg
-      | .congruenceFun => Tactic.congruenceFun
-      | .congruence => Tactic.congruence
-
-
-
 end Pantograph
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 21bffce..6a10309 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -286,7 +286,8 @@ protected def GoalState.serializeGoals
     | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 
 /-- Print the metavariables in a readable format -/
-protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM String := do
+@[export pantograph_goal_state_diag_m]
+protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): MetaM String := do
   goalState.restoreMetaM
   let savedState := goalState.savedState
   let goals := savedState.tactic.goals
@@ -305,7 +306,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
   let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
       !(goals.contains mvarId || mvarId == root) && options.printAll)
       |>.mapM (fun (mvarId, decl) => do
-        let pref := if goalState.newMVars.contains mvarId then "~" else " "
+        let pref := if parentHasMVar mvarId then " " else "~"
         printMVar pref mvarId decl
       )
   pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
@@ -345,5 +346,6 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
     userNameToString : Name → String
       | .anonymous => ""
       | other => s!"[{other}]"
+    parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
 
 end Pantograph
diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean
index 225ad31..8efebc8 100644
--- a/Pantograph/Tactic.lean
+++ b/Pantograph/Tactic.lean
@@ -1,4 +1,5 @@
 
+import Pantograph.Tactic.Assign
 import Pantograph.Tactic.Congruence
 import Pantograph.Tactic.MotivatedApply
 import Pantograph.Tactic.NoConfuse
diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean
new file mode 100644
index 0000000..cd9281f
--- /dev/null
+++ b/Pantograph/Tactic/Assign.lean
@@ -0,0 +1,35 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+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
+      assert! prevMVarDecl.type == mvarDecl.type
+      acc
+    else
+      acc.insert mvarId
+    ) SSet.empty
+def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do
+  goal.checkNotAssigned `Pantograph.Tactic.assign
+
+  -- This run of the unifier is critical in resolving mvars in passing
+  let exprType ← Meta.inferType expr
+  let goalType ← goal.getType
+  unless ← Meta.isDefEq goalType exprType do
+    throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
+
+  let nextGoals ← Meta.getMVars expr
+  goal.assign expr
+  nextGoals.toList.filterM (not <$> ·.isAssigned)
+
+def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
+  let goalType ← Elab.Tactic.getMainTarget
+  let expr ← Elab.Term.elabTermAndSynthesize (stx := stx) (expectedType? := .some goalType)
+  let nextGoals ← assign (← Elab.Tactic.getMainGoal) expr
+  Elab.Tactic.setGoals nextGoals
+
+
+end Pantograph.Tactic
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 4ac8454..3849b44 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -198,10 +198,10 @@ def test_proposition_generation: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
+    #[.some "∀ (x : Nat), ?m.29 x"])
   addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
 
-  let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
+  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := "fun x => Eq.refl x") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString