[opentheory-users] mapping names in opentheory

[Joe Hurd]

Hi Ramana,

I believe that all system-dependent interface infrastructure belongs
in the HOL theorem provers, not in OpenTheory. The hol-light.int file
in the opentheory repo is just used for regression testing, and really
belongs in the hol-light git repo I recently made available. I should
move it.

Cheers,

Joe

On Tue, Jan 11, 2011 at 2:13 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> On Mon, Jan 10, 2011 at 8:49 PM, Joe Hurd <joe at gilith.com> wrote:
>>But what I would expect is that you would have functions:
>>
>> importName : openTheoryName -> holName
>>
>> exportName : holName -> openTheoryName
>>
>> that you would always use for converting between HOL4 names and
>> OpenTheory names.
>
> I have started adding these functions to HOL4 (the dictionaries are
> there but not well-populated).
> But now I am wondering about test/interpretations/hol-light.int in the
> opentheory source repository.
> What is the point of this file, and where/how is it used?
> Is it an alternative method whereby the above functions are
> unrequired, each proof assistant only ever deals with its own names
> and reads/writes articles about them, and opentheory takes care of the
> renaming instead?
> If so, which method is preferred?
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>