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

[Tobias Nipkow]

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
>