Re: [isabelle] unhelpful comment in Term.ML
As the author of both the code and the comment, I can confirm that I always preferred to call this function with singleton lists.
> On 11 Nov 2015, at 09:31, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
> 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. ;)
This archive was generated by a fusion of
Pipermail (Mailman edition) and