[isabelle-dev] Products over lists – naming convention for big sums and products.
florian.haftmann at informatik.tu-muenchen.de
Thu Sep 25 16:32:15 CEST 2014
>>> 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.
The captialization is derived from existing Inf, Sup, Union, Inter (vs.
inf, sup, union, inter).
For binary operations like +, -, *, / there is a preference to prefer
the name of the operation (plus, mult) over the algebraic concept (sum,
product). But these are exceptions.
>> PS: Maybe c) could be tackled in the future when we have a hypothetical
>> constant/lemma renaming tool.
The issue is the renaming of lemmas, which is not so straighforward.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev