[isabelle-dev] Evaluation of floor and ceiling

[Brian Huffman]

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 <lp15 at cam.ac.uk> 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.
>
>