On 26/05/2014 11:07, Jasmin Blanchette wrote: > Am 26.05.2014 um 11:02 schrieb Tobias Nipkow <nip...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
