Copyright | (c) Conal Elliott 2009 |
---|---|
License | BSD3 |
Maintainer | conal@conal.net |
Stability | experimental |
Safe Haskell | Safe |
Language | Haskell98 |
Type equality proofs
- data (:=:) :: * -> * -> * where
- liftEq :: (a :=: a') -> f a :=: f a'
- liftEq2 :: (a :=: a') -> (b :=: b') -> f a b :=: f a' b'
- liftEq3 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> f a b c :=: f a' b' c'
- liftEq4 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> (d :=: d') -> f a b c d :=: f a' b' c' d'
- commEq :: (a :=: a') -> a' :=: a
- transEq :: (a :=: a') -> (a' :=: a'') -> a :=: a''
Documentation
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 '(,,)')