[isabelle-dev] Notes on datatype_new list

[Tobias Nipkow]

On 26/05/2014 11:07, Jasmin Blanchette wrote:
> Am 26.05.2014 um 11:02 schrieb Tobias Nipkow <nipkow at in.tum.de>:
> 
>> The definition of list should look like before.
> 
> I don't see how this is an option. This would result in the following duplicate constants:
> 
>     map_list vs. map
>     set_list vs. set
>     rel_list vs. forall_list2
>     un_Cons1 vs. hd
>     un_Cons2 vs. tl

Duplicate constants are not a killer argument per se. But why not generate those
constants only if the definer asks for them explicitly? Does any programming
language give you all of them by default? Have you made a study of existing
Isabelle datatypes to see how frequently people defined their own
map/set/rel/selectors? Concerning the selectors: the default names will almost
never be what the users wants and hence she will have to mention them anyway (if
she wants them).

Tobias