For one, I think it is confusing for users when the type class hierarchy changes from one release to the next.
Also, as a library writer, I think that the separation of classes archimedean_field and floor_ceiling would be annoying in the same way that the separation of comm_ring and number_ring is. It seems weird to have two different classes when they are logically equivalent in strength (i.e. no types are instances of one but not the other). - Brian On Fri, Jul 8, 2011 at 1:40 AM, Lawrence Paulson <[email protected]> wrote: > Is there any real cost to having so many type classes? > Larry > > On 8 Jul 2011, at 02:13, Brian Huffman wrote: > >> The drawback to this design is that it requires yet another type >> class, of which we have plenty already. > > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
