[opentheory-users] interpretation in separate file

[Joe Leslie-Hurd]

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
>