ty-0.1.4: Typed type representations and equality proofs

Stabilityexperimental
Maintainerconal@conal.net
Safe HaskellSafe-Inferred

Data.Proof.EQ

Description

Type equality proofs

Synopsis

Documentation

data :=: whereSource

Type equality proof

Constructors

Refl :: a :=: a 

liftEq :: (a :=: a') -> f a :=: f a'Source

Lift proof through a unary type constructor

liftEq2 :: (a :=: a') -> (b :=: b') -> f a b :=: f a' b'Source

Lift proof through a binary type constructor (including '(,)')

liftEq3 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> f a b c :=: f a' b' c'Source

Lift proof through a ternary type constructor (including '(,,)')

liftEq4 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> (d :=: d') -> f a b c d :=: f a' b' c' d'Source

Lift proof through a quaternary type constructor (including '(,,,)')

commEq :: (a :=: a') -> a' :=: aSource

Commutativity

transEq :: (a :=: a') -> (a' :=: a'') -> a :=: a''Source

Transitivity