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
instantiation lift :: (type) eq
Conflict of type arities for classes Representable.predomain <
Lift.lift :: (HOL.type)
Lift.lift :: (Countable.countable)
which I don't understand. What is happening here?
On 07/07/2012 01:04 PM, Christian Sternagel wrote:
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and