Data.Parameterized.DecidableEq

This defines a class DecidableEq, which represents decidable equality on a type family.

This is different from GHC's TestEquality in that it provides evidence of non-equality. In fact, it is a superclass of TestEquality.

Documentation

class DecidableEq f where

Decidable equality.

Methods

decEq :: f a -> f b -> Either (a :~: b) ((a :~: b) -> Void)

Instances

DecidableEq BoolRepr

Defined in Data.Parameterized.BoolRepr

Methods

decEq :: forall (a :: k) (b :: k). BoolRepr a -> BoolRepr b -> Either (a :~: b) ((a :~: b) -> Void)

DecidableEq NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

decEq :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Either (a :~: b) ((a :~: b) -> Void)

DecidableEq PeanoRepr

Defined in Data.Parameterized.Peano

Methods

decEq :: forall (a :: k) (b :: k). PeanoRepr a -> PeanoRepr b -> Either (a :~: b) ((a :~: b) -> Void)