[isabelle-dev] Products over lists – naming convention for big sums and products.
nipkow at in.tum.de
Thu Sep 25 07:32:33 CEST 2014
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
>> 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?
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.
> - 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.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev