parameterized-utils-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
LanguageHaskell98

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
DecidableEq BoolRepr Source # 
Instance details

Defined in Data.Parameterized.BoolRepr

Methods

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

DecidableEq NatRepr Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

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

DecidableEq PeanoRepr Source # 
Instance details

Defined in Data.Parameterized.Peano

Methods

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