*To*: Michael Norrish <Michael.Norrish at nicta.com.au>*Subject*: Re: [isabelle] unhelpful comment in Term.ML*From*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Date*: Wed, 11 Nov 2015 10:31:17 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <75FA1F3E-DB1C-4D7E-A53E-8A5BC37B672A@nicta.com.au>*References*: <DC2FC414-829D-4A26-B17E-3C68C6E694E8@nicta.com.au> <282EAE1C-93ED-4878-BFCC-619642F3D699@inria.fr> <75FA1F3E-DB1C-4D7E-A53E-8A5BC37B672A@nicta.com.au>

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

**Follow-Ups**:**Re: [isabelle] unhelpful comment in Term.ML***From:*Makarius

**Re: [isabelle] unhelpful comment in Term.ML***From:*Lawrence Paulson

**References**:**[isabelle] unhelpful comment in Term.ML***From:*Michael Norrish

**Re: [isabelle] unhelpful comment in Term.ML***From:*Jasmin Blanchette

**Re: [isabelle] unhelpful comment in Term.ML***From:*Michael Norrish

- Previous by Date: Re: [isabelle] unhelpful comment in Term.ML
- Next by Date: Re: [isabelle] unhelpful comment in Term.ML
- Previous by Thread: Re: [isabelle] unhelpful comment in Term.ML
- Next by Thread: Re: [isabelle] unhelpful comment in Term.ML
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list