parameterized-utils-2.1.11.0: Classes and data structures for working with data-kind indexed types

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 :: k -> Type) where
  - decEq :: forall (a :: k) (b :: k). f a -> f b -> Either (a :~: b) ((a :~: b) -> Void)

# Documentation

class DecidableEq (f :: k -> Type) where Source #

Decidable equality.

Methods

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

#### Instances

Instances details

DecidableEq NatRepr Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods decEq :: forall (a :: Nat) (b :: Nat). 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 :: Peano) (b :: Peano). 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 :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #