>>> 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.
What is the meaning of »modify« here? They are still the same. The change of the definition of foldl/foldr was a simple device to get correspondences between them and fold in particular; choosing *one* provisory proposal how to bootstrap them was simpler and faster (i.e. the »modification« created »less work«) than building an abstraction layer over two or three different developments. Choosing another bootstrap is still possible (if not easier than before) and can happen within a few minutes. Details and workload of big engineering tasks are hard to foresee anyway. Maybe in the future I would use something like http://live.gnome.org/ProjectHamster ? Again: personally I have no preference how to fold best, but I guess it is hard to write theorems like union_set_fold with a different argument order than that of what is now fold and foldr. I'm not reluctant to adjust the whole matter as soon as a coherent proposal is made. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
