[isabelle] type classes without class parameters

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)"

but then the resulting type of the class predicate is

  term class.infinite
    :: "'a itself ⇒ bool

I'm not sure whether this would make sense at all. My initial thought was to replace assumptions like

  assumes "infinite (UNIV :: 'a)"

by "'a :: infinite" in appropriate places.



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