宣言に [simp] 属性が付与されているかどうかチェックするコマンド

Zulip: request: discourage squeezing terminal simps?

import Lean

@[simp]
theorem X : True := trivial

open Lean Elab Command Meta in
elab "#is_simp " ids:ident+ : command => do
  let se := simpExtension.getState (← getEnv)
  for id in ids do
    let nm ← liftCoreM do realizeGlobalConstNoOverload id
    if se.lemmaNames.contains (.decl nm) then
      logInfoAt id m!"'{.ofConstName nm}' has the `simp` attribute!"
    else
      logWarningAt id m!"'{.ofConstName nm}' does not have the `simp` attribute!"

#is_simp X

attribute [local simp] Nat.succ_mul in
#is_simp X Nat Nat.succ_mul

#is_simp X Nat Nat.succ_mul

Start with the proposed #is_simp command and its Lean.Elab.Command and Lean.Meta APIs in the issue body. Check the examples for global and local simp attributes, then verify that the command reports whether each declaration has the attribute and handles unresolved identifiers appropriately.