Re: [isabelle] Isabelle Cookbook example



On Tue, Sep 14, 2010 at 1:17 PM, Makarius <makarius at sketis.net> wrote:

> 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.
>
>
I see. Could you tell me where '--' and the '>>' infix operators are
implemented?

Thanks
Steve


>        Makarius
>




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