公理がどこで導入されたかまで出力する `#print axioms` コマンドの亜種

Zulip: > Hunting down axioms

import Lean

open Lean

structure State where
  visited : NameSet    := {}
  axioms  : Array (Name × Name) := #[]

abbrev M := ReaderT Environment $ StateM State

partial def collect (origin : Name) (c : Name) : M Unit := do
  let collectExpr (origin : Name) (e : Expr) : M Unit := e.getUsedConstants.forM (collect origin)
  let s ← get
  unless s.visited.contains c do
    modify fun s => { s with visited := s.visited.insert c }
    let env ← read
    match env.find? c with
    | some (ConstantInfo.axiomInfo _)  => modify fun s => { s with axioms := s.axioms.push (origin, c) }
    | some (ConstantInfo.defnInfo v)   => collectExpr c v.type *> collectExpr c v.value
    | some (ConstantInfo.thmInfo v)    => collectExpr c v.type *> collectExpr c v.value
    | some (ConstantInfo.opaqueInfo v) => collectExpr c v.type *> collectExpr c v.value
    | some (ConstantInfo.quotInfo _)   => pure ()
    | some (ConstantInfo.ctorInfo v)   => collectExpr c v.type
    | some (ConstantInfo.recInfo v)    => collectExpr c v.type
    | some (ConstantInfo.inductInfo v) => collectExpr c v.type *> v.ctors.forM (collect c)
    | none                             => pure ()

def foo [Monad m] [MonadEnv m] (constName : Name) : m (Array (Name × Name)) := do
  let env ← getEnv
  let (_, s) := ((collect constName constName).run env).run {}
  return s.axioms



def hack : Nat := sorry


def bar : Nat := hack


def foobar : Nat := bar + bar

#eval show MetaM _ from do foo ``foobar

Start with the linked Zulip discussion and the Lean prototype in this issue, especially collect, foo, and the sample hack/bar/foobar declarations. Determine the appropriate command entry point and confirm that the finished variant reports each axiom together with the declaration through which it was introduced.