Re: [isabelle] Isabelle Cookbook example



On Mon, 13 Sep 2010, Steve W wrote:

"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.


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.


	Makarius





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