Lean4
/-- `getAllDependencies cmd id` takes a `Syntax` input `cmd` and returns the `NameSet` of all the
declaration names that are implied by
* the `SyntaxNodeKinds`,
* the attributes of `cmd` (if there are any),
* the identifiers contained in `cmd`,
* if `cmd` adds a declaration `d` to the environment, then also all the module names implied by `d`.
The argument `id` is expected to be an identifier.
It is used either for the internally generated name of a "nameless" `instance` or when parsing
an identifier representing the name of a declaration.
Note that the return value does not contain dependencies of the dependencies;
you can use `Lean.NameSet.transitivelyUsedConstants` to get those.
-/
def getAllDependencies (cmd id : Syntax) : CommandElabM NameSet := do
let env ← getEnv
let nm ← getDeclName cmd
return
(← getVisited nm) |>.append (← getVisited id.getId) |>.append (getSyntaxNodeKinds cmd) |>.append (getAttrs env cmd)
