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


-- | Unary natural numbers relying on the singletons infrastructure.
--   
--   Unary natural number relying on the <a>singletons</a> infrastructure.
--   More information about the general usage of singletons can be found on
--   the <a>singletons github</a> page.
@package singleton-nats
@version 0.4.0.4

module Data.Nat
data Nat
Z :: Nat
S :: Nat -> Nat
natPlus :: Nat -> Nat -> Nat
natMul :: Nat -> Nat -> Nat
natMinus :: Nat -> Nat -> Nat
natAbs :: Nat -> Nat
type SNat = (Sing :: Nat -> Type)

-- | The singleton kind-indexed data family.
class PNum a
class SNum a
data SSym0 (l_aceu :: TyFun Nat Nat)
SSym0KindInference :: SSym0
type SSym1 (t_acet :: Nat) = S t_acet
type ZSym0 = Z

-- | Provides a shorthand for <a>Nat</a>-s using <a>GHC.TypeLits</a>, for
--   example:
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Lit 3
--   Lit 3 :: Nat
--   = 'S ('S ('S 'Z))
--   </pre>
type SLit n = Sing (Lit n)

-- | Shorthand for <a>SNat</a> literals using <tt>TypeApplications</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; :set -XTypeApplications
--   
--   &gt;&gt;&gt; sLit @5
--   SS (SS (SS (SS (SS SZ))))
--   </pre>
sLit :: forall (n :: Nat). SingI (Lit n) => Sing (Lit n)
instance GHC.Classes.Ord Data.Nat.Nat
instance GHC.Show.Show Data.Nat.Nat
instance GHC.Classes.Eq Data.Nat.Nat
instance GHC.Show.Show (Data.Singletons.Sing n)
instance Data.Singletons.Prelude.Num.PNum Data.Nat.Nat
instance GHC.Classes.Eq (Data.Nat.SNat n)
instance GHC.Classes.Ord (Data.Nat.SNat n)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Nat.Compare_1627441706Sym0
instance Data.Singletons.Prelude.Ord.POrd Data.Nat.Nat
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Nat.Compare_1627441706Sym1
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Nat.NatMulSym1
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Nat.NatMulSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Nat.NatPlusSym1
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Nat.NatPlusSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Nat.NatMinusSym1
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Nat.NatMinusSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Nat.NatAbsSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Nat.SSym0
instance Data.Singletons.Prelude.Eq.PEq Data.Nat.Nat
instance Data.Singletons.SingKind Data.Nat.Nat
instance Data.Singletons.Prelude.Eq.SEq Data.Nat.Nat
instance Data.Singletons.Decide.SDecide Data.Nat.Nat
instance Data.Singletons.Prelude.Ord.SOrd Data.Nat.Nat => Data.Singletons.Prelude.Ord.SOrd Data.Nat.Nat
instance Data.Singletons.SingI 'Data.Nat.Z
instance Data.Singletons.SingI n => Data.Singletons.SingI ('Data.Nat.S n)
instance Data.Singletons.Prelude.Num.SNum Data.Nat.Nat
