Data.Comp.Param.Equality

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

Documentation

class PEq a where

Equality on parametric values. The equality test is performed inside the FreshM monad for generating fresh identifiers.

Minimal complete definition

peq

Methods

peq :: a -> a -> FreshM Bool

Instances

Eq a => PEq a

Defined in Data.Comp.Param.Equality

Methods

peq :: a -> a -> FreshM Bool

PEq a => PEq [a]

Defined in Data.Comp.Param.Equality

Methods

peq :: [a] -> [a] -> FreshM Bool

(EqD f, PEq a) => PEq (Cxt h f Name a)

Defined in Data.Comp.Param.Equality

Methods

peq :: Cxt h f Name a -> Cxt h f Name a -> FreshM Bool

class EqD f where

Signature equality. An instance EqD f gives rise to an instance Eq (Term f). The equality test is performed inside the FreshM monad for generating fresh identifiers.

Minimal complete definition

eqD

Methods

eqD :: PEq a => f Name a -> f Name a -> FreshM Bool

Instances

(EqD f, EqD g) => EqD (f :+: g)

EqD is propagated through sums.

Defined in Data.Comp.Param.Equality

Methods

eqD :: PEq a => (f :+: g) Name a -> (f :+: g) Name a -> FreshM Bool

EqD f => EqD (Cxt h f)

From an EqD difunctor an Eq instance of the corresponding term type can be derived.

Defined in Data.Comp.Param.Equality

Methods

eqD :: PEq a => Cxt h f Name a -> Cxt h f Name a -> FreshM Bool

Orphan instances

(Difunctor f, EqD f) => Eq (Term f)

Equality on terms.

Methods

(==) :: Term f -> Term f -> Bool

(/=) :: Term f -> Term f -> Bool