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

Lawrence Paulson lp15 at cam.ac.uk
Thu Sep 18 16:22:03 CEST 2014


A gain in legibility for sure.
Larry

On 18 Sep 2014, at 15:11, Tobias Nipkow <nipkow at 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 
>> 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)
> 
> Looking again at the result of our discussion I still like it.




More information about the isabelle-dev mailing list