Re: [isabelle] unhelpful comment in Term.ML

On Wed, 11 Nov 2015, Jasmin Blanchette 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. ;)

These comments belong indeed to ancient tradition from Cambridge. Over the years, we have fine-tuned many of them, and actually removed the majority -- because the informal text and the formal explanation in ML did not agree.

Term.subst_bounds looks a bit old and confusing in various respects, but it still has a correct reading in the historical context of term.ML, as already explained by Jasmin.

In general, Isabelle sources are understood as follows (in that order):

  (1) reading the definition in ML

  (2) looking through typical uses in ML

  (3) peeking at the informal snippets around the formal text, without
      taking them too seriously


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