Email Gateway (Aug 18 2022 at 12:54): Email Gateway (Aug 18 2022 at 12:54):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Is it possible to print all the attributes that are currently set for a
given theorem? I only found `print_attributes', but that doesn't take
any argument, does it?
cheers
christian
Email Gateway (Aug 18 2022 at 12:54):From: Makarius <makarius@sketis.net>
Attributes are essentially functions that operate on theorems (and the
implicit context), e.g. "simp" to add a thm to the part of the context
where the Simplifier looks later. These tools usually provide ways to
inspect this aspect of the context, e.g. 'print_simpset'.
Projecting the content of the universal context like that is the only way
to get to the desired information. In particular, attributes are not like
"tags" sticking to a theorem.
Makarius
Last updated: May 03 2024 at 01:09 UTC