Extracting out theorems tagged with an attribute

Stream: general

[l1mey]

I am interested in extracting out theorems that I tag with @[rewrite] in the same manner that Tao's Equational Theories project uses the extract_implications.lean or export_equations.lean. It is used in the CI like so to generate a list of equations:

image.png

I am guessing that on an attribute use, the registered attribute will add to a global list of implications or equations? EquationalResult.lean might have what I'm explaining.

The goal for my project is to formalise compiler rewrite rules, so I would define a theorem in Lean and use the @[rewrite] attribute to tag a theorem as a valid rewrite, given it's proven. For example:

@[rewrite]
theorem const_swap {u} (a b con1 con2 : BitVec u)
    : (a + con1) - (b + con2) = (a - b) + (con1 - con2) := by

  grind

It would be nice to be able to extract out all of these theorems, iterate over them, and output a list of valid rules to my liking. Just at the moment, I do not know how to implement an attribute that would do such a thing. The Lean metaprogramming handbook did not have anything on attributes and the reference wasn't too helpful either. Could anyone explain to me a basic skeleton for what needs to get done?

[Aaron Liu]

what I do in these kinds of situations is I find an attribute and I copy how it works

[l1mey]

I'm currently trying with the Equational Theories attributes, will let people know how it goes.

[Aaron Liu]

here's an example you can use docs#Mathlib.Meta.NormNum.normNumExt

[Oliver Dressler]

If you want another example, I had a similar situation in LeanRPC.
I define a custom attribute, then collect and process all functions tagged with it:
https://github.com/oOo0oOo/LeanRPC/blob/cfa37190964d4d3468ad6e293d9911af2009f053/LeanRPC/Attribute.lean#L22