Re: [isabelle] Isabelle Cookbook example



On Mon, 13 Sep 2010, Steve W wrote:

there's an example on implementing a custom antiquotation:

"let
val parser = Args.context

fun term_pat (ctxt, str) =
...

end"

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.


	Makarius





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