There is generic machinery for adding values of various forms to theories so
that future theories and ML code can see them. The smoothest instantiation is
in ThmSetData (in src/1) which allows storage of sets of theorems in a “2D
matrix” indexed by theory-name and set-name. For example, the automatic
rewrites behind the “simp” attribute are implemented this way.
The storage of grammar updates is handled with the same technology.
A hacky way to store terms would be to use theorems with conclusions of the
form
K T (myterm)
and to then use ThmSetData.
A better way, which, now that I’ve been prodded, I may implement soon, would be
to write a TermSetData.
I hope this helps. I’m happy to discuss the details of this relatively
undocumented feature further if you want more help.
Best wishes,
Michael
On 11/1/18, 01:51, "Heiko Becker" <hbec...@mpi-sws.org> wrote:
Hello everyone,
suppose I have a custom tactic that depends on a list of terms and I
want to keep adding elements to the list throughout my development.
I tried to achieve this using a :term list ref on the ML level. However,
it is the case that if I add some term in theory A and inspect the list
in theory B, where A is in the theory graph before B, all elements added
in A are not in the list anymore.
Can someone give me a hint on why this is the case or tell me a better
way to "share" a list of terms from a theory with theories depending on it?
Cheers,
Heiko
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
