Re: [isabelle] HOLCF equality


On 07/07/2012, at 2:51 PM, Christian Sternagel wrote:

> 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

HOLCF is built out on a series of type classes. The most basic class that supports the continuous function space constructor (->) is "cpo".

So the most general definition for your eq class is:

class eq = fixes eq :: "'a::cpo -> 'a -> tr"

I think you can find some discussion in the archives about what the default class is in HOLCF and why it is hard to get it right for all uses.



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