On 25.09.2014 18:32, Tobias Nipkow wrote:
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.
That would be »Sum_list« and »Prod_list«.
The idea of having »sum« and »prod« was inspired by
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
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.
One could argue that sets are the canonical indexing structure. On the other
hand, we have syntax to make the actual names irrelevant.
Larry
On 24 Sep 2014, at 11:18, Johannes Hölzl hoe...@in.tum.de wrote:
Why Sum and not Sum_set in c)? Is the intention that the canonical type
always gets
On 18/09/2014 15:47, Florian Haftmann wrote:
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:
A gain in legibility for sure.
Larry
On 18 Sep 2014, at 15:11, Tobias Nipkow nip...@in.tum.de wrote:
On 18/09/2014 15:47, Florian Haftmann wrote:
Changeset #fe083c681ed8 introduces products over lists. There has been
some private discussion whether there could be a serious attempt to
