[isabelle-dev] Evaluation of floor and ceiling
brianh at cs.pdx.edu
Fri Jul 8 14:43:06 CEST 2011
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).
On Fri, Jul 8, 2011 at 1:40 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> Is there any real cost to having so many type classes?
> 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.
More information about the isabelle-dev