Florian: But you agree that it should be uniformaly "Sum" or "sum" for all summation operators? Johannes already remarked on the discrepancy in your proposal.
Tobias On 25/09/2014 16:32, Florian Haftmann wrote: >>>> 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. >> >> Indeed. >> >>> And why upper case Sum instead of sum? >> >> I am less sure about that. Usually the capitalized versions are the Big >> operators, but "sum" is already big (the binary version is called "plus") >> and sum_list is also a big operator. Unless we have a clear and simple >> policy, all lowercase would be better. > > The captialization is derived from existing Inf, Sup, Union, Inter (vs. > inf, sup, union, inter). > > For binary operations like +, -, *, / there is a preference to prefer the > name of the operation (plus, mult) over the algebraic concept (sum, > product). But these are exceptions. > >>> PS: Maybe c) could be tackled in the future when we have a >>> hypothetical constant/lemma renaming tool. > > The issue is the renaming of lemmas, which is not so straighforward. > > 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