From 2dc7657e2a225564dba5887b3b82bf046c58c876 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 6 Dec 2023 15:05:04 -0800
Subject: [PATCH] doc: getUsedConstants bug about projections

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

diff --git a/Pantograph.lean b/Pantograph.lean
index 958e43c..a66db35 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -86,6 +86,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         type := ← serialize_expression state.options info.type,
         value? := ← value?.mapM (λ v => serialize_expression state.options v),
         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 => name_to_ast n) else .none,
         valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
         module? := module?