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

[Tobias Nipkow]

On 24/09/2014 12:18, Johannes Hölzl wrote:
> Am Donnerstag, den 18.09.2014, 15:47 +0200 schrieb Florian Haftmann:
>> Changeset #fe083c681ed8 introduces products over lists.  There has been
>> some private discussion whether there could be a serious attempt to
>> establish a new consistent naming scheme for summation and products over
>> collections.
>>
>> 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.

Tobias

>  - Johannes
> 
> PS: Maybe c) could be tackled in the future when we have a hypothetical
> constant/lemma renaming tool.
> 
>> As far as can be forseen, 58 theories would be affected by a switch as
>> suggested by a). b) is no big issue. c) is maybe beyond what should be
>> reasonably attempted (218 affected theories).
>> 	
>> Suggestions welcome.
>> 	
>> Cheers,
>> 	Florian
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>