Am Donnerstag, den 18.09.2014, 15:47 +0200 schrieb Florian Haftmann: > Changeset #fe083c681ed8 introduces products over lists. There has been > some private discussion whether there could be a serious attempt to > establish a new consistent naming scheme for summation and products over > collections. > > a) for lists: sum_list (← listsum), prod_list (← listprod) > b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod) > c) for finite sets: Sum (← setsum), Prod (← setprod)
I assume a) means Sum_list and Prod_list?! Why Sum and not Sum_set in c)? Is the intention that the canonical type always gets the short name? Like map instead of map_list. And why upper case Sum instead of sum? - Johannes PS: Maybe c) could be tackled in the future when we have a hypothetical constant/lemma renaming tool. > As far as can be forseen, 58 theories would be affected by a switch as > suggested by a). b) is no big issue. c) is maybe beyond what should be > reasonably attempted (218 affected theories). > > Suggestions welcome. > > Cheers, > Florian > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
