Re: [isabelle] type classes without class parameters
On Jul 25, 2013 9:30 AM, "Christian Sternagel" <c.sternagel at gmail.com>
> Dear all,
> is it possible to use type classes without any class parameters (i.e.,
> For example, something like
> class infinite =
> assumes infinite: "infinite (UNIV::'a set)"
Yes, that is certainly possible. See for example class "finite" from the
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and