From 8707dbc9bb09f42a6fe8739a0846b84e4941004f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 16 Jun 2024 13:44:57 -0700
Subject: [PATCH] fix: aux lemmas in env inspect

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

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index b696c25..d5cdc3d 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -52,21 +52,22 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
     | .some false, _ => .none
     | .none, .defnInfo _ => info.value?
     | .none, _ => .none
+  let type ← unfoldAuxLemmas info.type
+  let value? ← value?.mapM (λ v => unfoldAuxLemmas v)
   -- Information common to all symbols
   let core := {
-    type := ← (serializeExpression options info.type).run',
+    type := ← (serializeExpression options type).run',
     isUnsafe := info.isUnsafe,
     value? := ← value?.mapM (λ v => serializeExpression options v |>.run'),
     publicName? := Lean.privateToUserName? name |>.map (·.toString),
     -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
     typeDependency? := if args.dependency?.getD false
-      then .some <| info.type.getUsedConstants.map (λ n => serializeName n)
+      then .some <| type.getUsedConstants.map (λ n => serializeName n)
+      else .none,
+    valueDependency? := if args.dependency?.getD false
+      then value?.map (λ e =>
+        e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
       else .none,
-    valueDependency? := ← if args.dependency?.getD false
-      then info.value?.mapM (λ e => do
-        let e ← unfoldAuxLemmas e
-        pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
-      else pure (.none),
     module? := module?
   }
   let result ← match info with