Re: [Hol-info] Share list of terms with later theories

A related question: some time back I was looking at how datatypes are constructed, and found stuff in theory ind_type, and theorems like list_TY_DEF (which one finds by doing find "ty_def") But it seems that there are also theorems created which define the constructors of the list datatype in

Re: [Hol-info] Share list of terms with later theories

If people wanting to store these “uninteresting” theorems are happy to wrap and unwrap the OMITs, this would be one approach. I had been thinking of adding a save_private_thm(name, privatedbname, thm) entrypoint to Theory.sml. You’d want multiple possible “private dbs”, so there would

Re: [Hol-info] Share list of terms with later theories

Hi all, How about defining: OMIT x = x in markerScript.sml and making it print as ... and adjust HOL so that a theorem with a top-level OMIT does not show up in DB searches. Cheers, Magnus On 12 January 2018 at 00:00, wrote: > I was thinking along these

Re: [Hol-info] Share list of terms with later theories

I was thinking along these lines, yeah. Such theorems could also be stopped from appearing in the Theory.sig file. Michael On 12/1/18, 07:31, "Konrad Slind" wrote: Theorems that need to persist between sessions are most easily stored by name in theories.

Re: [Hol-info] Share list of terms with later theories

Theorems that need to persist between sessions are most easily stored by name in theories. Maybe some kind of PolyML database magic could also be used, I don't know. As far as DB searches, it wouldn't be hard to implement a refined DB search mechanism that first discarded all theorems that met

Re: [Hol-info] Share list of terms with later theories

Ah, I didn't realise this existed. Thanks for the pointers! How does storing of theorems work in this setting? One can't construct a theorem from a string in a decode function. I guess the string could refer to a theorem name that's stored in the theory, but this is a bit inconvenient because

Re: [Hol-info] Share list of terms with later theories

That level of generality is already possible, and has always been a desideratum for the design. (The grammar update information stored is about that complicated for example; consider the types that occur in a call to add_rule.) The painful part is that you have to write functions to encode and

[Hol-info] Share list of terms with later theories

Hi Michael, I see that you are considering to add a TermSetData feature. Could you please add something more general? I'd appreciate a feature that can store the CakeML translator's state in theories. Currently, the CakeML translator stores its state in a single theorem so that the other theories

Re: [Hol-info] Share list of terms with later theories

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

[Hol-info] Share list of terms with later theories

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