Safe Haskell	None
Language	Haskell2010

Data.Nat

Synopsis

data Nat
- = Z
- | S Nat
type family NatPlus (a :: Nat) (a :: Nat) :: Nat where ...
type family NatMul (a :: Nat) (a :: Nat) :: Nat where ...
type family NatMinus (a :: Nat) (a :: Nat) :: Nat where ...
type family NatAbs (a :: Nat) :: Nat where ...
type family NatSignum (a :: Nat) :: Nat where ...
natPlus :: Nat -> Nat -> Nat
natMul :: Nat -> Nat -> Nat
natMinus :: Nat -> Nat -> Nat
natAbs :: Nat -> Nat
natSignum :: Nat -> Nat
someNatVal :: Integer -> Maybe (SomeSing Nat)
type SNat = (Sing :: Nat -> Type)
data family Sing (a :: k) :: Type
class PNum a
class SNum a
data SSym0 :: (~>) Nat Nat where
- SSym0KindInference :: forall t6989586621679098622 arg. SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0 t6989586621679098622
type SSym1 (t6989586621679098622 :: Nat) = S t6989586621679098622
type ZSym0 = Z
type family Lit n where ...
data LitSym0 :: (~>) Nat Nat where
- LitSym0KindInference :: forall n6989586621679117734 arg. SameKind (Apply LitSym0 arg) (LitSym1 arg) => LitSym0 n6989586621679117734
type LitSym1 (n6989586621679117734 :: Nat) = Lit n6989586621679117734
type SLit n = Sing (Lit n)
sLit :: forall (n :: Nat). SingI (Lit n) => Sing (Lit n)

Documentation

data Nat #

Constructors

Z
S Nat

Instances

Eq Nat #
Instance details Defined in Data.Nat Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Num Nat #
Instance details Defined in Data.Nat Methods (+) :: Nat -> Nat -> Nat # (-) :: Nat -> Nat -> Nat # (*) :: Nat -> Nat -> Nat # negate :: Nat -> Nat # abs :: Nat -> Nat # signum :: Nat -> Nat # fromInteger :: Integer -> Nat #
Ord Nat #
Instance details Defined in Data.Nat Methods compare :: Nat -> Nat -> Ordering # (<) :: Nat -> Nat -> Bool # (<=) :: Nat -> Nat -> Bool # (>) :: Nat -> Nat -> Bool # (>=) :: Nat -> Nat -> Bool # max :: Nat -> Nat -> Nat # min :: Nat -> Nat -> Nat #
Show Nat #
Instance details Defined in Data.Nat Methods showsPrec :: Int -> Nat -> ShowS # show :: Nat -> String # showList :: [Nat] -> ShowS #
PShow Nat #
Instance details Defined in Data.Nat Associated Types type ShowsPrec arg arg1 arg2 :: Symbol # type Show_ arg :: Symbol # type ShowList arg arg1 :: Symbol #
SShow Nat => SShow Nat #
Instance details Defined in Data.Nat Methods sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) # sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) # sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) #
PNum Nat #
Instance details Defined in Data.Nat Associated Types type arg + arg1 :: a # type arg - arg1 :: a # type arg * arg1 :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #
SNum Nat #
Instance details Defined in Data.Nat Methods (%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) # sNegate :: Sing t -> Sing (Apply NegateSym0 t) # sAbs :: Sing t -> Sing (Apply AbsSym0 t) # sSignum :: Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #
POrd Nat #
Instance details Defined in Data.Nat Associated Types type Compare arg arg1 :: Ordering # type arg < arg1 :: Bool # type arg <= arg1 :: Bool # type arg > arg1 :: Bool # type arg >= arg1 :: Bool # type Max arg arg1 :: a # type Min arg arg1 :: a #
SOrd Nat => SOrd Nat #
Instance details Defined in Data.Nat Methods sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) # (%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) # (%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) # (%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) # (%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) # sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) # sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #
SEq Nat => SEq Nat #
Instance details Defined in Data.Nat Methods (%==) :: Sing a -> Sing b -> Sing (a == b) # (%/=) :: Sing a -> Sing b -> Sing (a /= b) #
PEq Nat #
Instance details Defined in Data.Nat Associated Types type x == y :: Bool # type x /= y :: Bool #
SDecide Nat => SDecide Nat #
Instance details Defined in Data.Nat Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
SingKind Nat #
Instance details Defined in Data.Nat Associated Types type Demote Nat = (r :: Type) # Methods fromSing :: Sing a -> Demote Nat # toSing :: Demote Nat -> SomeSing Nat #
SingI Z #
Instance details Defined in Data.Nat Methods sing :: Sing Z #
SingI n => SingI (S n :: Nat) #
Instance details Defined in Data.Nat Methods sing :: Sing (S n) #
Eq (SNat n) #
Instance details Defined in Data.Nat Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #
Ord (SNat n) #
Instance details Defined in Data.Nat Methods compare :: SNat n -> SNat n -> Ordering # (<) :: SNat n -> SNat n -> Bool # (<=) :: SNat n -> SNat n -> Bool # (>) :: SNat n -> SNat n -> Bool # (>=) :: SNat n -> SNat n -> Bool # max :: SNat n -> SNat n -> SNat n # min :: SNat n -> SNat n -> SNat n #
ShowSing Nat => Show (Sing z) #
Instance details Defined in Data.Nat Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
SuppressUnusedWarnings LitSym0 #
Instance details Defined in Data.Nat Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings SSym0 #
Instance details Defined in Data.Nat Methods suppressUnusedWarnings :: () #
SingI SSym0 #
Instance details Defined in Data.Nat Methods sing :: Sing SSym0 #
SingI (TyCon1 S) #
Instance details Defined in Data.Nat Methods sing :: Sing (TyCon1 S) #
data Sing (a :: Nat) #
Instance details Defined in Data.Nat data Sing (a :: Nat) where SZ :: forall (a :: Nat). Sing Z SS :: forall (a :: Nat) (n :: Nat). Sing n -> Sing (S n)
type Demote Nat #
Instance details Defined in Data.Nat type Demote Nat = Nat
type Show_ (arg :: Nat) #
Instance details Defined in Data.Nat type Show_ (arg :: Nat) = Apply (Show__6989586621680590298Sym0 :: TyFun Nat Symbol -> Type) arg
type FromInteger a #
Instance details Defined in Data.Nat type FromInteger a
type Signum (a :: Nat) #
Instance details Defined in Data.Nat type Signum (a :: Nat)
type Abs (a :: Nat) #
Instance details Defined in Data.Nat type Abs (a :: Nat)
type Negate (arg :: Nat) #
Instance details Defined in Data.Nat type Negate (arg :: Nat) = Apply (Negate_6989586621679951527Sym0 :: TyFun Nat Nat -> Type) arg
type ShowList (arg :: [Nat]) arg1 #
Instance details Defined in Data.Nat type ShowList (arg :: [Nat]) arg1 = Apply (Apply (ShowList_6989586621680590309Sym0 :: TyFun [Nat] (Symbol ~> Symbol) -> Type) arg) arg1
type (a1 :: Nat) * (a2 :: Nat) #
Instance details Defined in Data.Nat type (a1 :: Nat) * (a2 :: Nat)
type (a1 :: Nat) - (a2 :: Nat) #
Instance details Defined in Data.Nat type (a1 :: Nat) - (a2 :: Nat)
type (a1 :: Nat) + (a2 :: Nat) #
Instance details Defined in Data.Nat type (a1 :: Nat) + (a2 :: Nat)
type Min (arg :: Nat) (arg1 :: Nat) #
Instance details Defined in Data.Nat type Min (arg :: Nat) (arg1 :: Nat) = Apply (Apply (Min_6989586621679832061Sym0 :: TyFun Nat (Nat ~> Nat) -> Type) arg) arg1
type Max (arg :: Nat) (arg1 :: Nat) #
Instance details Defined in Data.Nat type Max (arg :: Nat) (arg1 :: Nat) = Apply (Apply (Max_6989586621679832043Sym0 :: TyFun Nat (Nat ~> Nat) -> Type) arg) arg1
type (arg :: Nat) >= (arg1 :: Nat) #
Instance details Defined in Data.Nat type (arg :: Nat) >= (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679832025Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg) arg1
type (arg :: Nat) > (arg1 :: Nat) #
Instance details Defined in Data.Nat type (arg :: Nat) > (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679832007Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg) arg1
type (arg :: Nat) <= (arg1 :: Nat) #
Instance details Defined in Data.Nat type (arg :: Nat) <= (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679831989Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg) arg1
type (arg :: Nat) < (arg1 :: Nat) #
Instance details Defined in Data.Nat type (arg :: Nat) < (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679831971Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg) arg1
type Compare (a1 :: Nat) (a2 :: Nat) #
Instance details Defined in Data.Nat type Compare (a1 :: Nat) (a2 :: Nat)
type (x :: Nat) /= (y :: Nat) #
Instance details Defined in Data.Nat type (x :: Nat) /= (y :: Nat) = Not (x == y)
type (a :: Nat) == (b :: Nat) #
Instance details Defined in Data.Nat type (a :: Nat) == (b :: Nat)
type ShowsPrec a1 (a2 :: Nat) a3 #
Instance details Defined in Data.Nat type ShowsPrec a1 (a2 :: Nat) a3
type Apply LitSym0 (n6989586621679117734 :: Nat) #
Instance details Defined in Data.Nat type Apply LitSym0 (n6989586621679117734 :: Nat) = Lit n6989586621679117734
type Apply SSym0 (t6989586621679098622 :: Nat) #
Instance details Defined in Data.Nat type Apply SSym0 (t6989586621679098622 :: Nat) = S t6989586621679098622

type family NatPlus (a :: Nat) (a :: Nat) :: Nat where ... #

Equations

NatPlus Z b = b
NatPlus (S a) b = Apply SSym0 (Apply (Apply NatPlusSym0 a) b)

type family NatMul (a :: Nat) (a :: Nat) :: Nat where ... #

Equations

NatMul Z _ = ZSym0
NatMul (S a) b = Apply (Apply NatPlusSym0 b) (Apply (Apply NatMulSym0 a) b)

type family NatMinus (a :: Nat) (a :: Nat) :: Nat where ... #

Equations

NatMinus Z _ = ZSym0
NatMinus (S a) (S b) = Apply (Apply NatMinusSym0 a) b
NatMinus a Z = a

type family NatAbs (a :: Nat) :: Nat where ... #

Equations

NatAbs n = n

type family NatSignum (a :: Nat) :: Nat where ... #

Equations

NatSignum Z = ZSym0
NatSignum (S _) = Apply SSym0 ZSym0

natPlus :: Nat -> Nat -> Nat #

natMul :: Nat -> Nat -> Nat #

natMinus :: Nat -> Nat -> Nat #

natAbs :: Nat -> Nat #

natSignum :: Nat -> Nat #

someNatVal :: Integer -> Maybe (SomeSing Nat) #

Converts a runtime Integer to an existentially wrapped Nat. Returns Nothing if the argument is negative

type SNat = (Sing :: Nat -> Type) #

data family Sing (a :: k) :: Type #

The singleton kind-indexed data family.

Instances

Eq (SNat n) #
Instance details Defined in Data.Nat Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #
Ord (SNat n) #
Instance details Defined in Data.Nat Methods compare :: SNat n -> SNat n -> Ordering # (<) :: SNat n -> SNat n -> Bool # (<=) :: SNat n -> SNat n -> Bool # (>) :: SNat n -> SNat n -> Bool # (>=) :: SNat n -> SNat n -> Bool # max :: SNat n -> SNat n -> SNat n # min :: SNat n -> SNat n -> SNat n #
ShowSing Nat => Show (Sing z) #
Instance details Defined in Data.Nat Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
data Sing (a :: Bool)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Bool) where SFalse :: forall (a :: Bool). Sing False STrue :: forall (a :: Bool). Sing True
data Sing (a :: Ordering)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Ordering) where SLT :: forall (a :: Ordering). Sing LT SEQ :: forall (a :: Ordering). Sing EQ SGT :: forall (a :: Ordering). Sing GT
data Sing (n :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: forall (n :: Nat). KnownNat n => Sing n
data Sing (n :: Symbol)
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: forall (n :: Symbol). KnownSymbol n => Sing n
data Sing (a :: ())
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: ()) where STuple0 :: forall (a :: ()). Sing ()
data Sing (a :: Nat) #
Instance details Defined in Data.Nat data Sing (a :: Nat) where SZ :: forall (a :: Nat). Sing Z SS :: forall (a :: Nat) (n :: Nat). Sing n -> Sing (S n)
data Sing (a :: Void)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Void)
data Sing (a :: All)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: All) where SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)
data Sing (a :: Any)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: Any) where SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)
data Sing (b :: [a])
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: [a]) where SNil :: forall a (b :: [a]). Sing ([] :: [a]) SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)
data Sing (b :: Maybe a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Maybe a) where SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a) SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)
data Sing (b :: Min a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Min a) where SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)
data Sing (b :: Max a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Max a) where SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)
data Sing (b :: First a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)
data Sing (b :: Last a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)
data Sing (a :: WrappedMonoid m)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)
data Sing (b :: Option a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Option a) where SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)
data Sing (b :: Identity a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Identity a) where SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)
data Sing (b :: First a)
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)
data Sing (b :: Last a)
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)
data Sing (b :: Dual a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Dual a) where SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)
data Sing (b :: Sum a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Sum a) where SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)
data Sing (b :: Product a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Product a) where SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)
data Sing (b :: Down a)
Instance details Defined in Data.Singletons.Prelude.Ord data Sing (b :: Down a) where SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)
data Sing (b :: NonEmpty a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: NonEmpty a) where (:%\|) :: forall a (b :: NonEmpty a) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 :\| n2)
data Sing (b :: Endo a)
Instance details Defined in Data.Singletons.Prelude.Foldable data Sing (b :: Endo a) where SEndo :: forall a (b :: Endo a) (x :: a ~> a). Sing x -> Sing (Endo x)
data Sing (b :: MinInternal a)
Instance details Defined in Data.Singletons.Prelude.Foldable data Sing (b :: MinInternal a) where SMinInternal :: forall a (b :: MinInternal a) (x :: Maybe a). Sing x -> Sing (MinInternal x)
data Sing (b :: MaxInternal a)
Instance details Defined in Data.Singletons.Prelude.Foldable data Sing (b :: MaxInternal a) where SMaxInternal :: forall a (b :: MaxInternal a) (x :: Maybe a). Sing x -> Sing (MaxInternal x)
data Sing (c :: Either a b)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: Either a b) where SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b) SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)
data Sing (c :: (a, b))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: (a, b)) where STuple2 :: forall a b (c :: (a, b)) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing ((,) n1 n2)
data Sing (c :: Arg a b)
Instance details Defined in Data.Singletons.Prelude.Semigroup data Sing (c :: Arg a b) where SArg :: forall a b (c :: Arg a b) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing (Arg n1 n2)
newtype Sing (f :: k1 ~> k2)
Instance details Defined in Data.Singletons.Internal newtype Sing (f :: k1 ~> k2) = SLambda { applySing :: forall (t :: k1). Sing t -> Sing (f @@ t) }
data Sing (b :: StateL s a)
Instance details Defined in Data.Singletons.Prelude.Traversable data Sing (b :: StateL s a) where SStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x)
data Sing (b :: StateR s a)
Instance details Defined in Data.Singletons.Prelude.Traversable data Sing (b :: StateR s a) where SStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x)
data Sing (d :: (a, b, c))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (d :: (a, b, c)) where STuple3 :: forall a b c (d :: (a, b, c)) (n1 :: a) (n2 :: b) (n3 :: c). Sing n1 -> Sing n2 -> Sing n3 -> Sing ((,,) n1 n2 n3)
data Sing (c :: Const a b)
Instance details Defined in Data.Singletons.Prelude.Const data Sing (c :: Const a b) where SConst :: forall k a (b :: k) (c :: Const a b) (a1 :: a). {..} -> Sing (Const a1 :: Const a b)
data Sing (e :: (a, b, c, d))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (e :: (a, b, c, d)) where STuple4 :: forall a b c d (e :: (a, b, c, d)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing ((,,,) n1 n2 n3 n4)
data Sing (f :: (a, b, c, d, e))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (f :: (a, b, c, d, e)) where STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing ((,,,,) n1 n2 n3 n4 n5)
data Sing (g :: (a, b, c, d, e, f))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (g :: (a, b, c, d, e, f)) where STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing ((,,,,,) n1 n2 n3 n4 n5 n6)
data Sing (h :: (a, b, c, d, e, f, g))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (h :: (a, b, c, d, e, f, g)) where STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f) (n7 :: g). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing n7 -> Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

class PNum a #

Instances

PNum Nat
Instance details Defined in Data.Singletons.Prelude.Num Associated Types type arg + arg1 :: a # type arg - arg1 :: a # type arg * arg1 :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #
PNum Nat #
Instance details Defined in Data.Nat Associated Types type arg + arg1 :: a # type arg - arg1 :: a # type arg * arg1 :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #
PNum (Down a)
Instance details Defined in Data.Singletons.Prelude.Num Associated Types type arg + arg1 :: a # type arg - arg1 :: a # type arg * arg1 :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #

class SNum a #

Minimal complete definition

(%+), (%*), sAbs, sSignum, sFromInteger

Instances

SNum Nat
Instance details Defined in Data.Singletons.Prelude.Num Methods (%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) # sNegate :: Sing t -> Sing (Apply NegateSym0 t) # sAbs :: Sing t -> Sing (Apply AbsSym0 t) # sSignum :: Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #
SNum Nat #
Instance details Defined in Data.Nat Methods (%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) # sNegate :: Sing t -> Sing (Apply NegateSym0 t) # sAbs :: Sing t -> Sing (Apply AbsSym0 t) # sSignum :: Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #
SNum a => SNum (Down a)
Instance details Defined in Data.Singletons.Prelude.Num Methods (%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) # sNegate :: Sing t -> Sing (Apply NegateSym0 t) # sAbs :: Sing t -> Sing (Apply AbsSym0 t) # sSignum :: Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #

data SSym0 :: (~>) Nat Nat where #

Constructors

SSym0KindInference :: forall t6989586621679098622 arg. SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0 t6989586621679098622

Instances

SuppressUnusedWarnings SSym0 #
Instance details Defined in Data.Nat Methods suppressUnusedWarnings :: () #
SingI SSym0 #
Instance details Defined in Data.Nat Methods sing :: Sing SSym0 #
type Apply SSym0 (t6989586621679098622 :: Nat) #
Instance details Defined in Data.Nat type Apply SSym0 (t6989586621679098622 :: Nat) = S t6989586621679098622

type SSym1 (t6989586621679098622 :: Nat) = S t6989586621679098622 #

type ZSym0 = Z #

type family Lit n where ... #

Provides a shorthand for Nat-s using GHC.TypeLits, for example:

>>> :kind! Lit 3
Lit 3 :: Nat
= 'S ('S ('S 'Z))

Equations

Lit 0 = Z
Lit n = S (Lit (n - 1))

data LitSym0 :: (~>) Nat Nat where #

Constructors

LitSym0KindInference :: forall n6989586621679117734 arg. SameKind (Apply LitSym0 arg) (LitSym1 arg) => LitSym0 n6989586621679117734

Instances

SuppressUnusedWarnings LitSym0 #
Instance details Defined in Data.Nat Methods suppressUnusedWarnings :: () #
type Apply LitSym0 (n6989586621679117734 :: Nat) #
Instance details Defined in Data.Nat type Apply LitSym0 (n6989586621679117734 :: Nat) = Lit n6989586621679117734

type LitSym1 (n6989586621679117734 :: Nat) = Lit n6989586621679117734 #

type SLit n = Sing (Lit n) #

sLit :: forall (n :: Nat). SingI (Lit n) => Sing (Lit n) #

Shorthand for SNat literals using TypeApplications.

>>> :set -XTypeApplications
>>> sLit @5
SS (SS (SS (SS (SS SZ))))