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


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

-- | Type-level <a>max</a>
type family Max (x :: Nat) (y :: Nat) :: Nat

-- | Type-level <a>min</a>
type family Min (x :: Nat) (y :: Nat) :: Nat

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

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

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

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

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

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

-- | Type-level equivalent of <a>integerLogBase#</a> where the operation
--   only reduces when:
--   
--   <pre>
--   <a>FLog</a> base value ~ <a>CLog</a> base value
--   </pre>
--   
--   Additionally, the following property holds for <a>Log</a>:
--   
--   <pre>
--   (base ^ (Log base value)) ~ value
--   </pre>
--   
--   Note that additional equations are provided by the type-checker plugin
--   solver <a>GHC.TypeLits.Extra.Solver</a>.
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 <a>GHC.TypeLits.Extra.Solver</a>.
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 <a>GHC.TypeLits.Extra.Solver</a>.
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
--   
--   <pre>
--   {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
--   </pre>
--   
--   pragma to the header of your file
module GHC.TypeLits.Extra.Solver

-- | A solver implement as a type-checker plugin for:
--   
--   <ul>
--   <li><a>Div</a>: type-level <a>div</a></li>
--   <li><a>Mod</a>: type-level <a>mod</a></li>
--   <li><a>FLog</a>: type-level equivalent of <a>integerLogBase#</a> .i.e.
--   the exact integer equivalent to "<tt><a>floor</a> (<a>logBase</a> x
--   y)</tt>"</li>
--   <li><a>CLog</a>: type-level equivalent of <i>the ceiling of</i>
--   <a>integerLogBase#</a> .i.e. the exact integer equivalent to
--   "<tt><a>ceiling</a> (<a>logBase</a> x y)</tt>"</li>
--   <li><a>Log</a>: type-level equivalent of <a>integerLogBase#</a> where
--   the operation only reduces when "<tt><a>floor</a> (<a>logBase</a> b x)
--   ~ <a>ceiling</a> (<a>logBase</a> b x)</tt>"</li>
--   <li><a>GCD</a>: a type-level <a>gcd</a></li>
--   <li><a>LCM</a>: a type-level <a>lcm</a></li>
--   </ul>
--   
--   To use the plugin, add
--   
--   <pre>
--   {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
--   </pre>
--   
--   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
