Pantograph/Library.lean

@@ -127,7 +127,7 @@ def exprEcho (expr: String) (options: @&Protocol.Options):
       | .error e => return .error e
       | .ok expr => pure expr
     try
-      let type ← instantiateAll (← Lean.Meta.inferType expr)
+      let type ← unfoldAuxLemmas (← Lean.Meta.inferType expr)
       return .ok {
           type := (← serialize_expression options type),
           expr := (← serialize_expression options expr)
@@ -171,9 +171,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
     state.restoreMetaM
     return {
       root? := ← state.rootExpr?.mapM (λ expr => do
-        serialize_expression options (← instantiateAll expr)),
+        serialize_expression options (← unfoldAuxLemmas expr)),
       parent? := ← state.parentExpr?.mapM (λ expr => do
-        serialize_expression options (← instantiateAll expr)),
+        serialize_expression options (← unfoldAuxLemmas expr)),
     }
   runMetaM metaM
 

Pantograph/Serial.lean

@@ -18,10 +18,6 @@ namespace Pantograph
 def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 
-def instantiateAll (e: Lean.Expr) : Lean.MetaM Lean.Expr := do
-  let e ← unfoldAuxLemmas e
-  instantiateMVars (← Lean.Meta.whnf e)
-
 --- Input Functions ---
 
 /-- Read syntax object from string -/