aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

doc: getUsedConstants bug about projections

This commit is contained in:
Leni Aniva 2023-12-06 15:05:04 -08:00
parent 8a8db545a5
commit 924a67f46d
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Pantograph.lean
View File

@ -86,6 +86,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
type := ← serialize_expression state.options info.type, type := ← serialize_expression state.options info.type,
value? := ← value?.mapM (λ v => serialize_expression state.options v), value? := ← value?.mapM (λ v => serialize_expression state.options v),
publicName? := Lean.privateToUserName? name |>.map (·.toString), 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, 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, valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
module? := module? module? := module?