Find why something depends on which axioms

This code is by Kyle Miller from https://is.gd/Ug5sXu

Importing this file provides a comment #axiom_blame that creates output like this:

#axiom_blame FinEnum.toList

'FinEnum.toList' depends on axioms:

* Quot.sound: FinEnum.toList → Equiv.instFunLike → Equiv.instFunLike.proof_1 → EquivLike.toFunLike → EquivLike.toFunLike.proof_1 → Function.LeftInverse.eq_rightInverse → Function.RightInverse.comp_eq_id → funext → Quot.sound

* Classical.choice: FinEnum.toList → List.finRange → List.finRange.proof_1 → List.mem_range → Init.Data.List.Nat.Range._auxLemma.10 → List.mem_range'_1 → Init.Data.List.Nat.Range._auxLemma.9 → List.mem_range' → Init.Data.Nat.Lemmas._auxLemma.9 → Nat.self_eq_add_left → Classical.propDecidable → Classical.choice

* propext: FinEnum.toList → List.finRange → List.finRange.proof_1 → List.mem_range → Init.Data.List.Nat.Range._auxLemma.10 → propext

structure CollectAxiomBlame.State : Type

• visited : Lean.NameSet
• axioms : Lean.NameMap (List Lean.Name)

@[reducible, inline]

abbrev CollectAxiomBlame.M (α : Type) : Type

Equations

• CollectAxiomBlame.M = ReaderT Lean.Environment (StateM CollectAxiomBlame.State)

partial def CollectAxiomBlame.collect (src : List Lean.Name) (c : Lean.Name) : M Unit

def «command#axiom_blame_» : Lean.ParserDescr

Equations

• «command#axiom_blame_» = Lean.ParserDescr.node `«command#axiom_blame_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#axiom_blame ") (Lean.ParserDescr.const `ident))