Stream: General

Topic: show theorems with certain attributes

view this post on Zulip Max W. Haslbeck (Sep 25 2019 at 13:23):

Is there any way to show all theorems with a certain attribute? For example all theorems with the fundef_cong attribute?

view this post on Zulip Kevin Kappelmann (Sep 26 2019 at 08:12):

My "solution" would be grep; but there might be something built-in I'm not aware of

view this post on Zulip Simon Wimmer (Sep 26 2019 at 12:26):

I believe the answer is 'no'.
For standard collections of named theorems, you can do

thm algebra_simps
thm transfer_raw

but for attributes that handle things on their own like fundef_cong,
there shouldn't be a way since attributes are just arbitrary code in the end.

Last updated: Aug 15 2022 at 02:13 UTC