[isabelle-dev] "canonical" left-fold combinator for lists

Tobias Nipkow nipkow at in.tum.de
Mon Feb 13 13:41:13 CET 2012

Am 13/02/2012 13:22, schrieb Florian Haftmann:
>>> Anyway, personally I have no strong opinion about this, so anybody who
>>> wants to get hands on should feel invited to do so.
>> It would have been better to discuss such a change beforehand rather
>> than make it and then say that we are welcome to modify it.
> Please recall:
>> The movement of the code setup for sets into the HOL-Main corpus also
>> brought this fold into List.thy.
> The task of introducing 'a set as type constructor was, as I still deem,
> too ambitious to depend on such a detail as the introduction of an
> additional definition into List.thy.

The irony is: if you had just added fold to List, without modifying
foldl/r, it would have been less work for you and we could have
discussed the unfication of the folds afterwards.


More information about the isabelle-dev mailing list