Re: [isabelle] Isabelle Cookbook example

On Mon, 13 Sep 2010, Steve W wrote:

there's an example on implementing a custom antiquotation:

val parser = Args.context

fun term_pat (ctxt, str) =


Then there's an example on calling this antiquotation:

@{term_pat "Suc (?x::nat)"}

Since term_pat takes two arguments ctxt and str, how come the antiquotation
@{term_pat "Suc (?x::nat)"} only has one argument?

The context is implicit here. The ML compilation takes place in a certain Isar text, and the formal context (at compile time) is derived from that position.


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