Getting all simprocs

Stream: metaprogramming / tactics

[Paul Lezeau]

Is there an easy/efficient way of getting all simprocs that are available given a current set of imports?
Basically, I'd be interested in something that does the same as docs#Lean.Meta.Simp.getSimprocs but also lists simprocs declared via simproc_decl rather than just simproc.

The context is #27392, which implements a command for finding all available simprocs that match on a given pattern.

[Robin Arnez]

simprocDeclExt but you also need to take the state of all modules into account:

import Mathlib

open Lean Meta Simp

def getAllSimprocs : Lean.CoreM (Array SimprocDecl) := do
  let env ← getEnv
  let state := simprocDeclExt.getState env
  let mut acc : Array SimprocDecl := #[]
  for (a, b) in state.builtin do
    acc := acc.push ⟨a, b⟩
  for (a, b) in state.newEntries do
    acc := acc.push ⟨a, b⟩
  for i in 0...env.header.modules.size do
    acc := acc ++ simprocDeclExt.getModuleEntries env i
  return acc

set_option pp.deepTerms true
#eval show CoreM _ from return ((← getAllSimprocs).map (·.declName)).qsort (fun a b => a.toString < b.toString)

[Paul Lezeau]

That's very helpful, thanks!