Copilot.Core.Type.Equality

Description

Propositional equality and type equality.

data Equal :: * -> * -> * where Source #

Propositional equality.

Constructors

class EqualType t where Source #

Type equality. If the value of x =~= y is Just Refl, then the two types x and y are equal.

x =~= y

Just Refl

x

y

Methods

(=~=) :: t a -> t b -> Maybe (Equal a b) Source #

Defined in Copilot.Core.Type

(=~=) :: Type a -> Type b -> Maybe (Equal a b) Source #

coerce :: Equal a b -> a -> b Source #

Safe coercion, which requires proof of equality.

refl :: Equal a a Source #

Proof of propositional equality.

trans :: Equal a b -> Equal b c -> Equal a c Source #

Transitivity.

symm :: Equal a b -> Equal b a Source #

Symmetry.

cong :: Equal a b -> Equal (f a) (f b) Source #

Congruence.