On 25.09.2014 18:32, Tobias Nipkow wrote: > 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.
That would be »Sum_list« and »Prod_list«. The idea of having »sum« and »prod« was inspired by plain functional programming. But uniformity seems indeed more important here than succinctness at any cost. Florian > > 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 > -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev