Re: [isabelle] type classes without class parameters

On Jul 25, 2013 9:30 AM, "Christian Sternagel" <c.sternagel at>
> Dear all,
> is it possible to use type classes without any class parameters (i.e.,
fixed constants)?
> For example, something like
>   class infinite =
>     assumes infinite: "infinite (UNIV::'a set)"

Yes, that is certainly possible. See for example class "finite" from the
standard libraries.

The problem with a type class for infinite types is that you can't quite
define the instances you want. For example, 'a*'b is infinite if either 'a
OR 'b is infinite, but you can't express this with an instance declaration.

- Brian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.