Re: [isabelle] const antiquotation

Hi Lucas,

> I noticed a strange behaviour with the const antiquotation:
> ML {* @{const "op ="} *} raises a TYPE exception.
> I was hoping it would give me the HOL constant for equality. Is there
> some easy rule of thumb about when the const antiquotation works and
> when it doesn't?

when using the const antiquotation, you must instantiate each of the
constant's type parameter:

  ML {* @{const "op =" ("'a")} *}

gives equality on 'a.

You could definitely argue that the error message could be more
informative.  I must also confess I can't remember what the original
motivation for this antiquotation was.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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