singleton-bool 0.1.0.0 → 0.1.1.0

raw patch · 3 files changed

+23/−2 lines, 3 files

Files

CHANGELOG.md +2/−0
singleton-bool.cabal +2/−1
src/Data/Singletons/Bool.hs +19/−1

+ CHANGELOG.md view

@@ -0,0 +1,2 @@+- 0.1.1.0+    - Add `eqToRefl`, `eqCast`, `trivialRefl`

singleton-bool.cabal view

@@ -3,7 +3,7 @@ -- see: https://github.com/sol/hpack  name:           singleton-bool-version:        0.1.0.0+version:        0.1.1.0 synopsis:       Type level booleans description:    Type level booleans.                 .@@ -21,6 +21,7 @@ cabal-version:  >= 1.10  extra-source-files:+  CHANGELOG.md   README.md  source-repository head

src/Data/Singletons/Bool.hs view

@@ -4,18 +4,24 @@ {-# LANGUAGE KindSignatures      #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators       #-}+#if __GLASGOW_HASKELL__ >= 800+{-# OPTIONS_GHC -Wno-redundant-constraints #-}+#endif module Data.Singletons.Bool (     SBool(..),     SBoolI(..),-    -- * Data.Type.Bool+    -- * Data.Type.Bool and .Equality     -- | These are only defined with @base >= 4.7@ #if MIN_VERSION_base(4,7,0)     sboolAnd, sboolOr, sboolNot,+    eqToRefl, eqCast, trivialRefl, #endif     ) where  #if MIN_VERSION_base(4,7,0) import           Data.Type.Bool+import           Data.Type.Equality+import           Unsafe.Coerce      (unsafeCoerce) #endif  data SBool (b :: Bool) where@@ -42,4 +48,16 @@ sboolNot :: SBool a -> SBool (Not a) sboolNot STrue  = SFalse sboolNot SFalse = STrue++-- | @since 0.1.1.0+eqToRefl :: (a == b) ~ 'True => a :~: b+eqToRefl = unsafeCoerce trivialRefl++-- | @since 0.1.1.0+eqCast :: (a == b) ~ 'True => a -> b+eqCast = unsafeCoerce++-- | @since 0.1.1.0+trivialRefl :: () :~: ()+trivialRefl = Refl #endif