Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ML antiquotations: let, note


view this post on Zulip Email Gateway (Aug 19 2022 at 11:03):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,

from isabelle doc implementation it is not clear to me what the
purpose of the two ML antiquotations @{let ...} and @{note ...} is.
Grepping over Isabelle's sources reveals that those are only used in the
manual itself. Could anybody clarify?

On a related note, I did not understand the description of the special
non-ASCII braces in the same part of the manual.

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 11:04):

From: Makarius <makarius@sketis.net>
Maybe the following paper helps to understand the greater context:
http://www4.in.tum.de/~wenzelm/papers/Isar-SML.pdf

There are some important ideas in the paper that are still not
implemented, notably ways to have ML abstraction over @{term} or @{typ}
(for functions or let expressions), or the speculative @{rule}
antiquotation that compiles Pure rules into ML functions in the manner of
old-style LCF/HOL systems.

There are also some things from that time that are implemented, but turned
out as non-essential. One could invent some half-decent applications for
the above (some kind of formally-checked ML preprocessor programming), but
the two or three cononical application scenarious are missing.

Makarius


Last updated: Mar 29 2024 at 04:18 UTC