Email Gateway (Aug 19 2022 at 15:46): Email Gateway (Aug 19 2022 at 15:46):From: Daniel Raggi <danielraggi@gmail.com>
How do I add or delete transfer rules at the ML level? I have found
functions Transfer.transfer_raw_add and Transfer.transfer_raw_del, but I've
realised that there must have been some renaming of the theorems when they
where added to the database of transfer rules, because the name I gave to
the theorems when declaring them doesn't work to add or remove them. So
what names can I use to access them?
I'm thinking that it's not just the name, but that something else has to be
done to the transfer rules to be usable by the transfer engine (adding
Transfer.Rel to rules that relate two constants?). This probably means that
if I want to add the rules at the ML level I also have to do that first. Am
I on the right track?
Thanks.
Daniel
Email Gateway (Aug 19 2022 at 15:46):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Daniel,
the default entry points are two attributes Transfer.transfer_add and
Transfer.transfer_del. They do internally some preprocessing and call
Transfer.transfer_raw_add (or Transfer.transfer_raw_del) at the end.
You shouldn't use Transfer.transfer_raw_add and
Transfer.transfer_raw_del unless you really know what you are doing.
Ad using the attributes:
If you are in a local_theory context, use Local_Theory.note. E.g.,
Local_Theory.note ((Binding.empty, [transfer_attr]), [transfer_rule])
where transfer_attr = Attrib.internal (K Transfer.transfer_add).
If you are in a global context, you can use Thm.attribute_declaration.
(e.g., Thm.attribute_declaration Transfer.transfer_add transfer_rule).
Ondrej
Email Gateway (Aug 19 2022 at 15:48):From: Daniel Raggi <danielraggi@gmail.com>
Thank you, Ondřej. Your suggestion worked.
Last updated: Apr 26 2024 at 16:20 UTC