Data.Comp.Equality

This module defines equality for signatures, which lifts to equality for terms and contexts.

Documentation

class EqF f where

Signature equality. An instance EqF f gives rise to an instance Eq (Term f).

Methods

eqF :: Eq a => f a -> f a -> Bool

Instances

EqF []

EqF Maybe

Eq a0 => EqF ((,) a)

(Eq a0, Eq b0) => EqF ((,,) a b)

EqF f => EqF (Cxt h f)

(Eq a0, Eq b0, Eq c0) => EqF ((,,,) a b c)

(EqF f, EqF g) => EqF ((:+:) * f g)

EqF is propagated through sums.

(Eq a0, Eq b0, Eq c0, Eq d0) => EqF ((,,,,) a b c d)

(Eq a0, Eq b0, Eq c0, Eq d0, Eq e0) => EqF ((,,,,,) a b c d e)

(Eq a0, Eq b0, Eq c0, Eq d0, Eq e0, Eq f0) => EqF ((,,,,,,) a b c d e f)

(Eq a0, Eq b0, Eq c0, Eq d0, Eq e0, Eq f0, Eq g0) => EqF ((,,,,,,,) a b c d e f g)

(Eq a0, Eq b0, Eq c0, Eq d0, Eq e0, Eq f0, Eq g0, Eq h0) => EqF ((,,,,,,,,) a b c d e f g h)

(Eq a0, Eq b0, Eq c0, Eq d0, Eq e0, Eq f0, Eq g0, Eq h0, Eq i0) => EqF ((,,,,,,,,,) a b c d e f g h i)

eqMod :: (EqF f, Functor f, Foldable f) => f a -> f b -> Maybe [(a, b)]

This function implements equality of values of type f a modulo the equality of a itself. If two functorial values are equal in this sense, eqMod returns a Just value containing a list of pairs consisting of corresponding components of the two functorial values.