# [isabelle-dev] Products over lists – naming convention for big sums and products.

Tobias Nipkow nipkow at in.tum.de
Thu Sep 25 18:32:19 CEST 2014

```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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

```