accessing theorems tagged by [match_pattern]

Stream: metaprogramming / tactics

[Moritz R]

Is there any way to get such a list?
I only found the map attributeMapRefwhich only gives me the
AttributeImpl - but match_pattern is probably a ParametricAttribute or something which builds on that (which has the wanted hasTag function), but i don't know how to receive that instance.

[Robin Arnez]

They are not theorems, but definitions, but here's your wish:

import Mathlib

open Lean
def Lean.TagAttribute.toArray (x : TagAttribute) : CoreM (Array Name) := do
  let env ← getEnv
  let num := env.header.modules.size
  let mut result := #[]
  for i in 0...num do
    result := result ++ x.ext.getModuleEntries env i
  result := result ++ (x.ext.getState env).toArray
  return result

#eval repr <$> Lean.matchPatternAttr.toArray

[Moritz R]

Thank you!

[Moritz R]

I guess my question boiled down to, 'where do you get the name matchPatternAttr from?'

[Robin Arnez]

#print matchPattern + autocompletion