`#print dependents`

command #

This is a variation on `#print axioms`

where one instead specifies the axioms to avoid,
and it prints a list of all the theorems in the file that depend on that axiom, and the list
of all theorems directly referenced that are "to blame" for this dependency. Useful for debugging
unexpected dependencies.

Collects the result of a `CollectDependents`

query.

- otherAxiom : Bool
If true, an axiom not in the initial list will be considered as marked.

- result : Lean.NameMap Bool
The cached results on visited constants.

## Instances For

The monad used by `CollectDependents`

.

## Equations

## Instances For

Constructs the initial state, marking the constants in `cs`

. The result of `collect`

will say
whether a given declaration depends transitively on one of these constants.

If `otherAxiom`

is true, any axiom not specified in `cs`

will also be tracked.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Collect the results for a given constant.

The command `#print dependents X Y`

prints a list of all the declarations in the file that
transitively depend on `X`

or `Y`

. After each declaration, it shows the list of all declarations
referred to directly in the body which also depend on `X`

or `Y`

.

For example, `#print axioms bar'`

below shows that `bar'`

depends on `Classical.choice`

, but not
why. `#print dependents Classical.choice`

says that `bar'`

depends on `Classical.choice`

because
it uses `foo`

and `foo`

uses `Classical.em`

. `bar`

is not listed because it is proved without using
`Classical.choice`

.

```
import Batteries.Tactic.PrintDependents
theorem foo : x = y ∨ x ≠ y := Classical.em _
theorem bar : 1 = 1 ∨ 1 ≠ 1 := by simp
theorem bar' : 1 = 1 ∨ 1 ≠ 1 := foo
#print axioms bar'
-- 'bar'' depends on axioms: [Classical.choice, Quot.sound, propext]
#print dependents Classical.choice
-- foo: Classical.em
-- bar': foo
```

## Equations

- One or more equations did not get rendered due to their size.