>>> 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
--
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
