parameterized-utils-2.1.2.0: Classes and data structures for working with data-kind indexed types
Copyright(c) Galois Inc 2014-2019
MaintainerLangston Barrett <langston@galois.com>
Safe HaskellSafe
LanguageHaskell2010

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

Documentation

class DecidableEq f where Source #

Decidable equality.

Methods

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

Instances

Instances details
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 #

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 #