From 3a534930894490d12248c4335d42cdf3e2baca56 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 5 Jun 2024 16:14:52 -0700
Subject: [PATCH] feat: Show delayed assignment in goal diag

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

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 8f56468..5cccb4e 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -329,11 +329,13 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
       let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
       let resultValue: String ←
         if options.printValue then
-          if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
+          if let .some value ← getExprMVarAssignment? mvarId then
             let value ← if options.instantiate
               then instantiateAll value
               else pure $ value
             pure s!"\n := {← Meta.ppExpr value}"
+          else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
+            pure s!"\n := $ {mvarIdPending.name}"
           else
             pure ""
         else