Re: [isabelle] Creating Theorems in ML

Hi Reto,

> thanks a lot for your pointers. I've managed to create a few theorems -- with the sorry goal for now.
> When I try to construct a datatype defined in HOL, I've got an undefined constant error in ML.
> What's the best approach in defining data types for the interoperability between HOL and ML?
> How can they be referred to directly?
> Scratch.thy:
>  datatype Foo = Bar string
> myml.ML:
>  ? Scratch.Bar "hello"

I have no idea what your overall application is, but I would infer from
your question »as it is« that it aims towards how to interface between
code generated from HOL and Isabelle/ML.

There is already substantial support for that use case, see particulary
the antiquotations @{code …} and various @{computation* …}.  See the
tutorial on code generation for details.

Note that if you are interested to generate native Isabelle/ML strings
you should adhere to type String.literal rather than string (the details
are delicate due to different notions of »string« in different target

Hope this helps in the next steps,

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.