Re: [isabelle] Splicing runtime ML values into Isar

> This looks like an interesting experiment. Do you think that something
> similar could be done for formal comments inside types and terms, i.e.,
> to change from the term language to the language context "document", as
> discussed in a thread from last year?

Certainly. I only discovered that terms may contain cartouches by
accident, but given that, the possibilities for embedded syntax are endless:

  syntax "_doc" :: "cartouche_position â 'a â 'a" ("DOC _ (_)")

This allows you to write

  term "(DOC âabcâ 3) + 4"

Of course, a suitable parse translation is required to make some sense
of "abc".


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