Email Gateway (Aug 18 2022 at 15:25): Email Gateway (Aug 18 2022 at 15:25):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Hi,
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?
(This is in both Isabelle-2009-2 and Isabelle-2009-1)
cheers,
lucas
Email Gateway (Aug 18 2022 at 15:25):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lucas,
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
signature.asc
Email Gateway (Aug 18 2022 at 15:25):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 19 2024 at 16:20 UTC