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

-- | Additional type-level operations on GHC.TypeLits.Nat
--   
--   Additional type-level operations on GHC.TypeLits.Nat:
--   
--   
--   
- Max: type-level max
--   
- Min: type-level min
--   
- Div: type-level div
--   
- Mod: type-level mod
--   
- FLog: type-level equivalent of integerLogBase#
--   i.e. the exact integer equivalent to floor (logBase x y)
--   
- CLog: type-level equivalent of the ceiling of
--   integerLogBase# i.e. the exact integer equivalent to
--   ceiling (logBase x y)
--   
- Log: type-level equivalent of integerLogBase#
--   where the operation only reduces when floor (logBase b x) ~
--   ceiling (logBase b x)
--   
- GCD: a type-level gcd
--   
- LCM: a type-level lcm
--   
--   
--   And a custom solver for the above operations defined in
--   GHC.TypeLits.Extra.Solver as a GHC type-checker plugin. To
--   use the plugin, add the
--   
--   
--   OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver
--   
--   
--   pragma to the header of your file.
@package ghc-typelits-extra
@version 0.4.8

-- | Additional type-level operations on Nat:
--   
--   
--   
- Max: type-level max
--   
- Min: type-level min
--   
- Div: type-level div
--   
- Mod: type-level mod
--   
- FLog: type-level equivalent of integerLogBase# .i.e.
--   the exact integer equivalent to "floor (logBase x
--   y)"
--   
- CLog: type-level equivalent of the ceiling of
--   integerLogBase# .i.e. the exact integer equivalent to
--   "ceiling (logBase x y)"
--   
- Log: type-level equivalent of integerLogBase# where
--   the operation only reduces when "floor (logBase b x)
--   ~ ceiling (logBase b x)"
--   
- GCD: a type-level gcd
--   
- LCM: a type-level lcm
--   
--   
--   A custom solver for the above operations defined is defined in
--   GHC.TypeLits.Extra.Solver as a GHC type-checker plugin. To use
--   the plugin, add the
--   
--   
--   {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
--   
--   
--   pragma to the header of your file.
module GHC.TypeLits.Extra

-- | Type-level max
type family Max (x :: Nat) (y :: Nat) :: Nat

-- | Type-level min
type family Min (x :: Nat) (y :: Nat) :: Nat

-- | Division (round down) of natural numbers. Div x 0 is
--   undefined (i.e., it cannot be reduced).
type family Div (a :: Natural) (b :: Natural) :: Natural
infixl 7 `Div`

-- | Modulus of natural numbers. Mod x 0 is undefined (i.e., it
--   cannot be reduced).
type family Mod (a :: Natural) (b :: Natural) :: Natural
infixl 7 `Mod`

-- | Type-level divMod
type DivMod (n :: Natural) (d :: Natural) = '(Div n d, Mod n d)

-- | A variant of Div that rounds up instead of down
type DivRU (n :: Natural) (d :: Natural) = Div n + d - 1 d

-- | Type-level equivalent of integerLogBase# .i.e. the exact
--   integer equivalent to "floor (logBase base
--   value)"
--   
--   Note that additional equations are provided by the type-checker plugin
--   solver GHC.TypeLits.Extra.Solver.
type family FLog (base :: Nat) (value :: Nat) :: Nat

-- | Type-level equivalent of the ceiling of integerLogBase#
--   .i.e. the exact integer equivalent to "ceiling
--   (logBase base value)"
--   
--   Note that additional equations are provided by the type-checker plugin
--   solver GHC.TypeLits.Extra.Solver.
type family CLog (base :: Nat) (value :: Nat) :: Nat

-- | Type-level equivalent of integerLogBase# where the operation
--   only reduces when:
--   
--   
--   FLog base value ~ CLog base value
--   
--   
--   Additionally, the following property holds for Log:
--   
--   
--   (base ^ (Log base value)) ~ value
--   
--   
--   Note that additional equations are provided by the type-checker plugin
--   solver GHC.TypeLits.Extra.Solver.
type family Log (base :: Nat) (value :: Nat) :: Nat

-- | Type-level greatest common denominator (GCD).
--   
--   Note that additional equations are provided by the type-checker plugin
--   solver GHC.TypeLits.Extra.Solver.
type family GCD (x :: Nat) (y :: Nat) :: Nat

-- | Type-level least common multiple (LCM).
--   
--   Note that additional equations are provided by the type-checker plugin
--   solver GHC.TypeLits.Extra.Solver.
type family LCM (x :: Nat) (y :: Nat) :: Nat
instance (GHC.Internal.TypeNats.KnownNat x, GHC.Internal.TypeNats.KnownNat y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeLits.Extra.Min" x y
instance (GHC.Internal.TypeNats.KnownNat x, GHC.Internal.TypeNats.KnownNat y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeLits.Extra.Max" x y
instance (GHC.Internal.TypeNats.KnownNat x, GHC.Internal.TypeNats.KnownNat y, GHC.TypeLits.Extra.FLog x y GHC.Types.~ GHC.TypeLits.Extra.CLog x y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeLits.Extra.Log" x y
instance (GHC.Internal.TypeNats.KnownNat x, GHC.Internal.TypeNats.KnownNat y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeLits.Extra.LCM" x y
instance (GHC.Internal.TypeNats.KnownNat x, GHC.Internal.TypeNats.KnownNat y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeLits.Extra.GCD" x y
instance (GHC.Internal.TypeNats.KnownNat x, GHC.Internal.TypeNats.KnownNat y, 2 GHC.Internal.Data.Type.Ord.<= x, 1 GHC.Internal.Data.Type.Ord.<= y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeLits.Extra.FLog" x y
instance (GHC.Internal.TypeNats.KnownNat x, GHC.Internal.TypeNats.KnownNat y, (2 GHC.Internal.Data.Type.Ord.<= x) GHC.Types.~ (() :: Constraint), 1 GHC.Internal.Data.Type.Ord.<= y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeLits.Extra.CLog" x y

-- | To use the plugin, add the
--   
--   
--   {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
--   
--   
--   pragma to the header of your file
module GHC.TypeLits.Extra.Solver

-- | A solver implement as a type-checker plugin for:
--   
--   
--   
- Div: type-level div
--   
- Mod: type-level mod
--   
- FLog: type-level equivalent of integerLogBase# .i.e.
--   the exact integer equivalent to "floor (logBase x
--   y)"
--   
- CLog: type-level equivalent of the ceiling of
--   integerLogBase# .i.e. the exact integer equivalent to
--   "ceiling (logBase x y)"
--   
- Log: type-level equivalent of integerLogBase# where
--   the operation only reduces when "floor (logBase b x)
--   ~ ceiling (logBase b x)"
--   
- GCD: a type-level gcd
--   
- LCM: a type-level lcm
--   
--   
--   To use the plugin, add
--   
--   
--   {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
--   
--   
--   To the header of your file.
plugin :: Plugin
instance GHC.Utils.Outputable.Outputable GHC.TypeLits.Extra.Solver.SimplifyResult
instance GHC.Utils.Outputable.Outputable GHC.TypeLits.Extra.Solver.SolverConstraint
