On Fri, 13 Jan 2012, Brian Huffman wrote:
I am writing about the following recent changeset, which adds another
left-fold operator to HOL/List.thy.
author haftmann
Fri Jan 06 10:19:49 2012 +0100 (6 days ago)
changeset 46133 d9fe85d3d2cd
parent 46132 5a29dbf4c155
child 46134 4b9d4659228a
incorporated canonical fold combinator on lists into body of List
theory; refactored passages on List.fold(l/r)
http://isabelle.in.tum.de/repos/isabelle/rev/d9fe85d3d2cd
I would like to take issue with a couple of things here. First, I
don't understand why it should be called "canonical". What mainstream
programming language has a left-fold operation with this particular
type signature? The only place I have ever seen this variety of fold
is in src/Pure/General/basics.ML in the Isabelle distribution.
"Canonical" is a technical term from the Isabelle/ML culture. The idea
behind it is already firmly established for many years, the name is there
for quite a few years as well. The Isabelle/Isar Implementation Manual
privides some text on this in section 0.3. (Does anybody have a PDF to
Stone-Tablet-Printer?)
I've never claimed myself that the HOL library or any other language out
there is or has to be canonical in that sense, although it would do them
good.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
