Re: [isabelle] const antiquotation



On Wed, 30 Jun 2010, Florian Haftmann wrote:

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.

It seems to be occasionally used to ensure that some @{term foo} in ML is actually a term constant, not a variable. There are other means to achive that within the regular term language: e.g. using qualified names, or the CONST marker of inner syntax. So @{term "CONST foo"} would also do the job, despite being a bit unwieldy compared to @{const foo}.


	Makarius






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