Re: [isabelle] Isabelle Cookbook example



On Mon, Sep 13, 2010 at 7:32 PM, Makarius <makarius at sketis.net> wrote:

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

Thanks

>
>        Makarius
>




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