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

[Johannes Hölzl]

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.

And why upper case Sum instead of sum?

 - 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