type-equality 0.1.1 → 0.1.2

raw patch · 3 files changed

+10/−1 lines, 3 files

Files

CHANGELOG +3/−0
src/Data/Type/Equality.hs +6/−0
type-equality.cabal +1/−1

CHANGELOG view

@@ -1,3 +1,6 @@+0.1.2+  * Add subst2. Thanks to James Koppel.+ 0.1.1   * Turn on PolyKinds for GHC >= 7.6. Thanks to Ben Franksen.

src/Data/Type/Equality.hs view

@@ -23,6 +23,7 @@   , sym   , trans   , subst+  , subst2      , cong   , cong2@@ -79,6 +80,11 @@ -- be defined as 'coerce' '.' 'cong'. subst :: a :=: b -> f a -> f b subst Refl = id++-- | Substitution inside nested type constructors. This is equivalent +-- to 'coerce' '.' 'cong' '.' 'cong'.+subst2 :: a :=: b -> f (g a) -> f (g b)+subst2 Refl = id  -- | Equality is congruential. cong :: a :=: b -> f a :=: f b

type-equality.cabal view

@@ -1,5 +1,5 @@ Name:                type-equality-Version:             0.1.1+Version:             0.1.2 Synopsis:            Type equality, coercion/cast and other operations. Description:         In the presence of GADTs, sometimes a proof is                      needed that two types are equal. This package