Data.Comp.Param.Multi.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 i -> a j -> FreshM Bool

Instances

PEq Name

Defined in Data.Comp.Param.Multi.Equality

Methods

peq :: Name i -> Name j -> FreshM Bool

Eq a => PEq (K a)

Defined in Data.Comp.Param.Multi.Equality

Methods

peq :: K a i -> K a j -> FreshM Bool

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

Defined in Data.Comp.Param.Multi.Equality

Methods

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

class EqHD f where

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

Minimal complete definition

eqHD

Methods

eqHD :: PEq a => f Name a i -> f Name a j -> FreshM Bool

Instances

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

EqHD is propagated through sums.

Defined in Data.Comp.Param.Multi.Equality

Methods

eqHD :: PEq a => (f :+: g) Name a i -> (f :+: g) Name a j -> FreshM Bool

EqHD f => EqHD (Cxt h f)

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

Defined in Data.Comp.Param.Multi.Equality

Methods

eqHD :: PEq a => Cxt h f Name a i -> Cxt h f Name a j -> FreshM Bool

Orphan instances

(HDifunctor f, EqHD f) => Eq (Term f i)

Equality on terms.

Methods

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

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