[opentheory-users] interpretation in separate file

[Ramana Kumar]

Hi Joe,

I would like to reopen this request. It seems like I'm going to be copying
interpretations around a lot again.

Cheers,
Ramana

On 4 March 2016 at 12:14, Ramana Kumar <ramana at member.fsf.org> wrote:

> Hi Joe,
>
> It turns out this is not so urgent for me since Michael and I came up with
> another method:
> Put all the article-combination stuff into one file uninterpreted.thy
> (main block is a union), then turn that into uninterpreted.art, and finally
> do the interpretation all at once (so it only appears in one file) in
> interpreted.thy, whose main block is an article block for
> "uninterpreted.art".
>
> However, interpretations from files would probably still be good for other
> scenarios. I would tweak your suggested syntax to use "interpretation"
> rather than "interpret-file", to match "article" (which also takes a
> filename).
>
> Cheers,
> Ramana
>
> On 5 March 2016 at 05:51, Joe Leslie-Hurd <joe at gilith.com> wrote:
>
>> Hi Ramana,
>>
>> I agree with you that it would be good for theory files to support
>> pulling in interpretations from files. How about the following syntax:
>>
>> interpret-file: "file.int"
>>
>> inside a theory block? It probably makes sense to allow multiple of
>> these, just like multiple
>>
>> interpret: type/const "X" as "Y"
>>
>> lines are allowed, but raise an error if the same symbol is
>> interpreted in multiple ways.
>>
>> Cheers,
>>
>> Joe
>>
>> On Thu, Mar 3, 2016 at 4:21 PM, Ramana Kumar <ramana at member.fsf.org>
>> wrote:
>> > Is it possible to include an interpretation in a theory file, rather
>> than
>> > having to write it out inline? Since I sometimes want to include a
>> rather
>> > large interpretation within multiple blocks within the same theory
>> file, I
>> > end up having to write a template file and then generate the real .thy
>> file
>> > from that, to avoid lots of copy-pasting. Is mine the recommended
>> approach,
>> > or is there a better way?
>> >
>> > _______________________________________________
>> > opentheory-users mailing list
>> > opentheory-users at gilith.com
>> > http://www.gilith.com/opentheory/mailing-list
>> >
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160401/a107fd13/attachment-0001.html>