[opentheory-users] mapping names in opentheory

[Joe Hurd]

Hi Ramana,

Further to this, I've moved the hol-light.int file to my instrumented
version of HOL Light, and made a new release of opentheory with a
little less cruft.

Cheers,

Joe

On Tue, Jan 11, 2011 at 2:27 PM, Joe Hurd <joe at gilith.com> wrote:
> 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
>>
>