[isabelle-dev] Products over lists – naming convention for big sums and products.
hoelzl at in.tum.de
Wed Sep 24 12:18:32 CEST 2014
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?
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
More information about the isabelle-dev