コマンド作例：choice を使っているかチェックするコマンド

[Seasawher]

see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20check.20dependency.20on.20axiom.20of.20choice/near/403799144

import Lean

open Lean Meta Elab Command

private def detectClassicalOf (constName : Name) : CommandElabM Unit := do
  let env ← getEnv
  let (_, s) := ((CollectAxioms.collect constName).run env).run {}
  if s.axioms.isEmpty then
    logInfo m!"'{constName}' does not depend on any axioms"
  else
    let caxes := s.axioms.filter fun nm => Name.isPrefixOf `Classical nm
    if caxes.isEmpty then
      logInfo m!"'{constName}' is non-classical and depends on axioms: {s.axioms.toList}"
    else
      throwError m!"'{constName}' depends on classical axioms: {caxes.toList}"

syntax (name:=detectClassical) "#detect_classical " ident : command

@[command_elab «detectClassical»] def elabDetectClassical : CommandElab
  | `(#detect_classical%$tk $id) => withRef tk do
    let cs ← resolveGlobalConstWithInfos id
    cs.forM detectClassicalOf
  | _ => throwUnsupportedSyntax

/-
Info:
> 'Nat.add' does not depend on any axioms
-/
#detect_classical Nat.add

/-
Info:
> 'Nat.div_add_mod' is non-classical and depends on axioms: [propext]
-/
#detect_classical Nat.div_add_mod

/-
Error:
> 'Nat.log2' depends on classical axioms: [Classical.choice]
-/
#detect_classical Nat.log2

[Seasawher]

ただし，これは v4.9.0-rc1 では動作しないようだ