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.