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
This archive was generated by a fusion of
Pipermail (Mailman edition) and