Re: [isabelle] HOLCF equality



When trying to define my own type class (I dropped all axioms for the sake of a minimal example)

class eq =
  fixes eq :: "'a → 'a → tr"

and instantiating the lift type

declare [[names_long]]

instantiation lift :: (type) eq
begin

I obtain

Conflict of type arities for classes Representable.predomain <
                   Bifinite.profinite:
  Lift.lift :: (HOL.type)
    Representable.predomain and
  Lift.lift :: (Countable.countable)
    Bifinite.profinite

which I don't understand. What is happening here?

cheers

chris

On 07/07/2012 01:04 PM, Christian Sternagel wrote:
Dear all,

is there already something like Haskell's "Eq" typeclass for HOLCF
(which seems to be neccessariy/convenient to formalize typical Haskell
functions). If not, are there any other reasons than lack of time?

cheers

chris








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