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,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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