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


-- | Integers bounded by a closed interval
--   
--   Integers bounded by a closed interval
@package closed
@version 0.2.0

module Closed.Internal
newtype Closed (n :: Nat) (m :: Nat)
Closed :: Integer -> Closed
[getClosed] :: Closed -> Integer

-- | Describe whether the endpoint of a <a>Bounds</a> includes or excludes
--   its argument
data Endpoint

-- | Endpoint includes its argument
Inclusive :: Nat -> Endpoint

-- | Endpoint excludes its argument
Exclusive :: Nat -> Endpoint

-- | Syntactic sugar to express open and half-open intervals using the
--   <a>Closed</a> type

-- | Syntactic sugar to express a value that has only one non-bottom
--   inhabitant using the <a>Closed</a> type
type Single (n :: Nat) = Bounds ( 'Inclusive n) ( 'Inclusive n)

-- | Syntactic sugar to express a value whose lower bound is zero
type FiniteNat (rhs :: Endpoint) = Bounds ( 'Inclusive 0) rhs

-- | Proxy for the lower bound of a <a>Closed</a> value
lowerBound :: Closed n m -> Proxy n

-- | Proxy for the upper bound of a <a>Closed</a> value
upperBound :: Closed n m -> Proxy m

-- | Safely create a <a>Closed</a> value using the specified argument
closed :: forall n m. (n <= m, KnownNat n, KnownNat m) => Integer -> Maybe (Closed n m)

-- | Create a <a>Closed</a> value throwing an error if the argument is not
--   in range
unsafeClosed :: forall n m. (HasCallStack, n <= m, KnownNat n, KnownNat m) => Integer -> Closed n m

-- | Test equality on <a>Closed</a> values in the same range

-- | Compare <a>Closed</a> values in the same range

-- | Generate the lowest and highest inhabitant of a given <a>Closed</a>
--   type

-- | Enumerate values in the range of a given <a>Closed</a> type

-- | Bounded arithmetic, e.g. maxBound + 1 == maxBound
unrepresentable :: (KnownNat n, KnownNat m) => Integer -> Closed n m -> String -> String

-- | Convert a type-level literal into a <a>Closed</a> value
natToClosed :: forall n m x proxy. (n <= x, x <= m, KnownNat x, KnownNat n, KnownNat m) => proxy x -> Closed n m

-- | Add inhabitants at the end
weakenUpper :: forall k n m. (n <= m, m <= k) => Closed n m -> Closed n k

-- | Add inhabitants at the beginning
weakenLower :: forall k n m. (n <= m, k <= n) => Closed n m -> Closed k m

-- | Remove inhabitants from the end. Returns <a>Nothing</a> if the input
--   was removed
strengthenUpper :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed n k)

-- | Remove inhabitants from the beginning. Returns <a>Nothing</a> if the
--   input was removed
strengthenLower :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed k m)

-- | Test two different types of <a>Closed</a> values for equality.
equals :: Closed n m -> Closed o p -> Bool
infix 4 `equals`

-- | Compare two different types of <a>Closed</a> values
cmp :: Closed n m -> Closed o p -> Ordering

-- | Add two different types of <a>Closed</a> values
add :: Closed n m -> Closed o p -> Closed (n + o) (m + p)

-- | Subtract two different types of <a>Closed</a> values Returns
--   <a>Left</a> for negative results, and <a>Right</a> for positive
--   results.
sub :: Closed n m -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))

-- | Multiply two different types of <a>Closed</a> values
multiply :: Closed n m -> Closed o p -> Closed (n * o) (m * p)

-- | Verifies that a given <a>Closed</a> value is valid. Should always
--   return <a>True</a> unles you bring the <tt>Closed.Internal.Closed</tt>
--   constructor into scope, or use <a>unsafeCoerce</a> or other nasty
--   hacks
isValidClosed :: (KnownNat n, KnownNat m) => Closed n m -> Bool
instance GHC.Generics.Generic (Closed.Internal.Closed n m)
instance GHC.Classes.Eq (Closed.Internal.Closed n m)
instance GHC.Classes.Ord (Closed.Internal.Closed n m)
instance (n GHC.TypeNats.<= m, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => GHC.Enum.Bounded (Closed.Internal.Closed n m)
instance (n GHC.TypeNats.<= m, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => GHC.Enum.Enum (Closed.Internal.Closed n m)
instance GHC.Show.Show (Closed.Internal.Closed n m)
instance (n GHC.TypeNats.<= m, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => GHC.Num.Num (Closed.Internal.Closed n m)
instance (n GHC.TypeNats.<= m, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => GHC.Real.Real (Closed.Internal.Closed n m)
instance (n GHC.TypeNats.<= m, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => GHC.Real.Integral (Closed.Internal.Closed n m)
instance Control.DeepSeq.NFData (Closed.Internal.Closed n m)
instance Data.Hashable.Class.Hashable (Closed.Internal.Closed n m)
instance Data.Aeson.Types.Class.ToJSON (Closed.Internal.Closed n m)
instance (n GHC.TypeNats.<= m, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => Data.Aeson.Types.Class.FromJSON (Closed.Internal.Closed n m)
instance Data.Csv.Conversion.ToField (Closed.Internal.Closed n m)
instance (n GHC.TypeNats.<= m, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => Data.Csv.Conversion.FromField (Closed.Internal.Closed n m)
instance (n GHC.TypeNats.<= m, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => Test.QuickCheck.Arbitrary.Arbitrary (Closed.Internal.Closed n m)
instance (n GHC.TypeNats.<= m, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => Database.Persist.Class.PersistField.PersistField (Closed.Internal.Closed n m)
instance (n GHC.TypeNats.<= m, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => Database.Persist.Sql.Class.PersistFieldSql (Closed.Internal.Closed n m)

module Closed

-- | Describe whether the endpoint of a <a>Bounds</a> includes or excludes
--   its argument
data Endpoint

-- | Endpoint includes its argument
Inclusive :: Nat -> Endpoint

-- | Endpoint excludes its argument
Exclusive :: Nat -> Endpoint
data Closed (n :: Nat) (m :: Nat)

-- | Syntactic sugar to express open and half-open intervals using the
--   <a>Closed</a> type

-- | Syntactic sugar to express a value that has only one non-bottom
--   inhabitant using the <a>Closed</a> type
type Single (n :: Nat) = Bounds ( 'Inclusive n) ( 'Inclusive n)

-- | Syntactic sugar to express a value whose lower bound is zero
type FiniteNat (rhs :: Endpoint) = Bounds ( 'Inclusive 0) rhs

-- | Safely create a <a>Closed</a> value using the specified argument
closed :: forall n m. (n <= m, KnownNat n, KnownNat m) => Integer -> Maybe (Closed n m)

-- | Create a <a>Closed</a> value throwing an error if the argument is not
--   in range
unsafeClosed :: forall n m. (HasCallStack, n <= m, KnownNat n, KnownNat m) => Integer -> Closed n m
getClosed :: Closed n m -> Integer

-- | Proxy for the lower bound of a <a>Closed</a> value
lowerBound :: Closed n m -> Proxy n

-- | Proxy for the upper bound of a <a>Closed</a> value
upperBound :: Closed n m -> Proxy m

-- | Test two different types of <a>Closed</a> values for equality.
equals :: Closed n m -> Closed o p -> Bool
infix 4 `equals`

-- | Compare two different types of <a>Closed</a> values
cmp :: Closed n m -> Closed o p -> Ordering

-- | Convert a type-level literal into a <a>Closed</a> value
natToClosed :: forall n m x proxy. (n <= x, x <= m, KnownNat x, KnownNat n, KnownNat m) => proxy x -> Closed n m

-- | Add inhabitants at the end
weakenUpper :: forall k n m. (n <= m, m <= k) => Closed n m -> Closed n k

-- | Add inhabitants at the beginning
weakenLower :: forall k n m. (n <= m, k <= n) => Closed n m -> Closed k m

-- | Remove inhabitants from the end. Returns <a>Nothing</a> if the input
--   was removed
strengthenUpper :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed n k)

-- | Remove inhabitants from the beginning. Returns <a>Nothing</a> if the
--   input was removed
strengthenLower :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed k m)

-- | Add two different types of <a>Closed</a> values
add :: Closed n m -> Closed o p -> Closed (n + o) (m + p)

-- | Subtract two different types of <a>Closed</a> values Returns
--   <a>Left</a> for negative results, and <a>Right</a> for positive
--   results.
sub :: Closed n m -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))

-- | Multiply two different types of <a>Closed</a> values
multiply :: Closed n m -> Closed o p -> Closed (n * o) (m * p)

-- | Verifies that a given <a>Closed</a> value is valid. Should always
--   return <a>True</a> unles you bring the <tt>Closed.Internal.Closed</tt>
--   constructor into scope, or use <a>unsafeCoerce</a> or other nasty
--   hacks
isValidClosed :: (KnownNat n, KnownNat m) => Closed n m -> Bool