OAlg.Data.EqualExtensional

Description

extensional equality.

Synopsis

class EqExt (c :: Type -> Type -> Type) where
- (.=.) :: c x y -> c x y -> Statement
prpEqualExt :: (Show x, Eq y) => X x -> (x -> y) -> (x -> y) -> Statement

Documentation

class EqExt (c :: Type -> Type -> Type) where Source #

extensional equality for two parameterized types.

Properties Let EqExt c then for all x, y holds:

For all f in c x y holdst: f .=. f.
For all f, g in c x y holdst: If f .=. g then holds g .=. f.
For all f, g and h in c x y holds: If f .=. g and g .=. h then f .=. h.

Minimal complete definition

Nothing

Methods

(.=.) :: c x y -> c x y -> Statement infix 4 Source #

equality statement of two objects.

default (.=.) :: Eq2 c => c x y -> c x y -> Statement Source #

Instances details

EqExt EqualExt Source #
Instance details Defined in OAlg.Data.Validable Methods (.=.) :: EqualExt x y -> EqualExt x y -> Statement Source #
EqExt EntEmpty2 Source #
Instance details Defined in OAlg.Entity.Definition Methods (.=.) :: EntEmpty2 x y -> EntEmpty2 x y -> Statement Source #
EqExt EqualExtOrt Source #
Instance details Defined in OAlg.Structure.Oriented.Definition Methods (.=.) :: EqualExtOrt x y -> EqualExtOrt x y -> Statement Source #
EqExt (HomEmpty s) Source #
Instance details Defined in OAlg.Hom.Definition Methods (.=.) :: HomEmpty s x y -> HomEmpty s x y -> Statement Source #
Transformable s Typ => EqExt (HomDisjEmpty s Op) Source #
Instance details Defined in OAlg.Hom.Definition Methods (.=.) :: HomDisjEmpty s Op x y -> HomDisjEmpty s Op x y -> Statement Source #

prpEqualExt :: (Show x, Eq y) => X x -> (x -> y) -> (x -> y) -> Statement Source #

validity for two functions being extensional equal, i.e. for all f and g in x -> y and x in x holds: f x == g y.