Copyright	(c) Galois Inc 2014-2019
Maintainer	Langston Barrett <langston@galois.com>
Safe Haskell	Safe
Language	Haskell2010

Data.Parameterized.DecidableEq

Description

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.

Synopsis

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

Documentation

Decidable equality.

Methods

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

Instances details

DecidableEq NatRepr Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods decEq :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #
DecidableEq PeanoRepr Source #
Instance details Defined in Data.Parameterized.Peano Methods decEq :: forall (a :: k) (b :: k). PeanoRepr a -> PeanoRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #
DecidableEq BoolRepr Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods decEq :: forall (a :: k) (b :: k). BoolRepr a -> BoolRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #