[opentheory-users] interpretation in separate file

[Ramana Kumar]

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/20160305/3b55b7ae/attachment.html>