Re: [isabelle] Isabelle Cookbook example

On Mon, 13 Sep 2010, Steve W wrote:

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
@{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

I see. Even if the context is implicit, does the position of the argument 'str' not matter? 'str' is the second argument of term_pat, but "Suc (?x::nat)" is in the first position in @{term_pat "Suc (?x::nat)"}.

I do not really understand the question. The parser for the antiquotation is defined like this:

  val parser = Args.context -- Scan.lift Args.name_source

This means it produces a pair (ctxt, str) in exactly that way. The context for Args.context is provided by the infrastructure -- these parsers are context-sensitive.


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