Re: [isabelle] unhelpful comment in Term.ML



>> I believe the comment is fine, or at least internally consistent. The second line does say "replacing (Bound i) with (argi)", which is what you found out too.
>> 
>> The first half of line 2, about "beta-reduction of arg(n-1)...arg0 into t", did not immediately deliver its meaning to me, but the example "subst_bounds([b,a], c)" (with [b, a] and not [a, b]) illustrates what is meant. In your example, this means you must write
>> 
>>   Term.subst_bounds ([ at {term "f::'a => 'b"}, @{term "x::'a"}], Bound 0 $ Bound 1)
>> 
>> to obtain f $ x, which is consistent with the beta-reduction
>> 
>>   (%y g. g y) x f == f x
>> 
>> i.e. the beta-redex has x f, the list argument to "subst_bounds" has [f, x] in reverse (cf. arg(n-1)...arg0).
> 
> Right, but why does it then list the args in the order
> 
>  arg(n-1), ... arg1, arg0
> 
> ?

Well, the input list is always [args0, ..., args(n-1)]. It's just the corresponding "beta-reduction" that takes the elements in reverse. This could be clearer, but when reading the text under the assumption that "args0" is the first element of the input list (which is reasonable), everything makes sense.

I'm not sure I'd dare to touch any old Larry (?) documentation, but if anybody is willing to clarify the text, I certainly won't stop them. ;)

Jasmin





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