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

  • otherAxiom : Bool

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

  • The cached results on visited constants.

Collects the result of a CollectDependents query.

Instances For
    @[inline, reducible]

    The monad used by CollectDependents.

    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.

      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 Std.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
        Instances For