-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | Decidable propositions.
--   
--   This package provides a Dec type.
--   
--   
--   type Neg a = a -> Void
--   
--   data Dec a
--       = Yes a
--       | No (Neg a)
--   
@package dec
@version 0.0.6

module Data.Type.Dec

-- | Intuitionistic negation.
type Neg a = a -> Void

-- | Decidable (nullary) relations.
data Dec a
Yes :: a -> Dec a
No :: Neg a -> Dec a

-- | Class of decidable types.
--   
--   
Law
--   
--   a should be a Proposition, i.e. the Yes answers should
--   be unique.
--   
--   Note: We'd want to have decidable equality :~: here
--   too, but that seems to be a deep dive into singletons.
class Decidable a
decide :: Decidable a => Dec a

-- | We can negate anything twice.
--   
--   Double-negation elimination is inverse of toNegNeg and
--   generally impossible.
toNegNeg :: a -> Neg (Neg a)

-- | Triple negation can be reduced to a single one.
tripleNeg :: Neg (Neg (Neg a)) -> Neg a

-- | Weak contradiction.
contradict :: (a -> Neg b) -> b -> Neg a

-- | A variant of contraposition.
contraposition :: (a -> b) -> Neg b -> Neg a

-- | Flip Dec branches.
decNeg :: Dec a -> Dec (Neg a)

-- | Show Dec.
--   
--   
--   >>> decShow $ Yes ()
--   "Yes ()"
--   
--   
--   
--   >>> decShow $ No id
--   "No <toVoid>"
--   
decShow :: Show a => Dec a -> String

-- | Convert Dec a to Maybe a, forgetting
--   the No evidence.
decToMaybe :: Dec a -> Maybe a

-- | Convert Dec to Bool, forgetting the evidence.
decToBool :: Dec a -> Bool

-- | Yes, it's boring.
boringYes :: Boring a => Dec a

-- | No, it's absurd.
absurdNo :: Absurd a => Dec a
instance Data.Type.Dec.Decidable a => Data.Boring.Boring (Data.Type.Dec.Dec a)
instance (Data.Type.Dec.Decidable a, Data.Type.Dec.Decidable b) => Data.Type.Dec.Decidable (a, b)
instance Data.Type.Dec.Decidable ()
instance Data.Type.Dec.Decidable GHC.Internal.Base.Void
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Type.Dec.Dec a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Type.Dec.Dec a)
