doc: getUsedConstants bug about projections

2023-12-06 15:05:04 -08:00 · 2023-12-06 15:05:04 -08:00 · 2dc7657e2a
parent ccf5a03647
commit 2dc7657e2a
1 changed files with 1 additions and 0 deletions
--- 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?