Re: [isabelle] signature of ml_antiquotation.ML: inline, value, embedded, etc.

On 11/10/2021 12:13, Kevin Kappelmann wrote:
> I fail to understand the signature provided by
> `Pure/ML/ml_antiquotation.ML` (see below).
> Can someone explain the meaning of `declaration`, `inline`, `value`, and
> `special_form`? Moreover, what is the meaning of `embedded` (e.g.
> `inline` vs `inline_embedded`)?

Isabelle sources are written for the human reader, but one needs to read them

  0. Overview: read the signatures as entries in "table of contents" of a
module (not as "specifications").

  1. Look inside: the definitions in the body tell how things are constructed
from more basic things. Usually there are extra headlines and other clues in
the source text.

  2. Look outside: do a hypersearch in Isabelle/jEdit as "induction over the
sources" to see how certain items are being used. This implicitly defines
intended semantics for them, and provides examples.

> val special_form: binding -> string -> theory -> theory

I don't see this in the published Isabelle2021, which is the implicit context
of this mailing list. If you have a different version, you need to say which one.

The terminology "special form" is standard in LISP.

The terminology "embedded" refers to Isabelle embedded languages, normally via
cartouches. The idea is also from LISP, but the syntax from myself after
staying > 3 years in France.


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