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

[Tobias Nipkow]

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.

Tobias