#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.

structure Batteries.Tactic.CollectDependents.State : Type

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.

@[reducible, inline]

abbrev Batteries.Tactic.CollectDependents.M (α : Type) : Type

The monad used by CollectDependents.

Equations

• Batteries.Tactic.CollectDependents.M = ReaderT Lean.Environment (StateM Batteries.Tactic.CollectDependents.State)

def Batteries.Tactic.CollectDependents.mkState (cs : Array (Lean.Name × Bool)) (otherAxiom : optParam Bool true) : Batteries.Tactic.CollectDependents.State

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.

partial def Batteries.Tactic.CollectDependents.collect (c : Lean.Name) : Batteries.Tactic.CollectDependents.M Bool

Collect the results for a given constant.

def Batteries.Tactic.«command#printDependents___» : Lean.ParserDescr

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.