Data.Nat

Documentation

data Nat

Constructors

Z

S Nat

Instances

Eq Nat

Defined in Data.Nat

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Num Nat

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

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

Defined in Data.Nat

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

PShow Nat

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

Defined in Data.Nat

Methods

sShowsPrec :: forall (t1 :: Nat0) (t2 :: Nat) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)

sShow_ :: forall (t :: Nat). Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: forall (t1 :: [Nat]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2)

PNum Nat

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

Defined in Data.Nat

Methods

(%+) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)

(%-) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2)

(%*) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)

sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t)

sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t)

sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t)

sFromInteger :: forall (t :: Nat0). Sing t -> Sing (Apply FromIntegerSym0 t)

POrd Nat

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

Defined in Data.Nat

Methods

sCompare :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

SEq Nat => SEq Nat

Defined in Data.Nat

Methods

(%==) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a == b)

(%/=) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a /= b)

PEq Nat

Defined in Data.Nat

Associated Types

type x == y :: Bool

type x /= y :: Bool

SDecide Nat => SDecide Nat

Defined in Data.Nat

Methods

(%~) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Decision (a :~: b)

SingKind Nat

Defined in Data.Nat

Associated Types

type Demote Nat = (r :: Type)

Methods

fromSing :: forall (a :: Nat). Sing a -> Demote Nat

toSing :: Demote Nat -> SomeSing Nat

SDecide Nat => TestCoercion SNat

Defined in Data.Nat

Methods

testCoercion :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (Coercion a b)

SDecide Nat => TestEquality SNat

Defined in Data.Nat

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

SingI 'Z

Defined in Data.Nat

Methods

sing :: Sing 'Z

SingI n => SingI ('S n :: Nat)

Defined in Data.Nat

Methods

sing :: Sing ('S n)

SuppressUnusedWarnings LitSym0

Defined in Data.Nat

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings SSym0

Defined in Data.Nat

Methods

suppressUnusedWarnings :: ()

SingI SSym0

Defined in Data.Nat

Methods

sing :: Sing SSym0

type Sing

Defined in Data.Nat

type Sing = SNat

type Demote Nat

Defined in Data.Nat

type Demote Nat = Nat

type Show_ (arg :: Nat)

Defined in Data.Nat

type Show_ (arg :: Nat) = Apply (Show__6989586621680289856Sym0 :: TyFun Nat Symbol -> Type) arg

type FromInteger a

Defined in Data.Nat

type FromInteger a

type Signum (a :: Nat)

Defined in Data.Nat

type Signum (a :: Nat)

type Abs (a :: Nat)

Defined in Data.Nat

type Abs (a :: Nat)

type Negate (arg :: Nat)

Defined in Data.Nat

type Negate (arg :: Nat) = Apply (Negate_6989586621679531293Sym0 :: TyFun Nat Nat -> Type) arg

type ShowList (arg :: [Nat]) arg1

Defined in Data.Nat

type ShowList (arg :: [Nat]) arg1 = Apply (Apply (ShowList_6989586621680289864Sym0 :: TyFun [Nat] (Symbol ~> Symbol) -> Type) arg) arg1

type (a1 :: Nat) * (a2 :: Nat)

Defined in Data.Nat

type (a1 :: Nat) * (a2 :: Nat)

type (a1 :: Nat) - (a2 :: Nat)

Defined in Data.Nat

type (a1 :: Nat) - (a2 :: Nat)

type (a1 :: Nat) + (a2 :: Nat)

Defined in Data.Nat

type (a1 :: Nat) + (a2 :: Nat)

type Min (arg :: Nat) (arg1 :: Nat)

Defined in Data.Nat

type Min (arg :: Nat) (arg1 :: Nat) = Apply (Apply (Min_6989586621679392900Sym0 :: TyFun Nat (Nat ~> Nat) -> Type) arg) arg1

type Max (arg :: Nat) (arg1 :: Nat)

Defined in Data.Nat

type Max (arg :: Nat) (arg1 :: Nat) = Apply (Apply (Max_6989586621679392884Sym0 :: TyFun Nat (Nat ~> Nat) -> Type) arg) arg1

type (arg :: Nat) >= (arg1 :: Nat)

Defined in Data.Nat

type (arg :: Nat) >= (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679392868Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg) arg1

type (arg :: Nat) > (arg1 :: Nat)

Defined in Data.Nat

type (arg :: Nat) > (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679392852Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg) arg1

type (arg :: Nat) <= (arg1 :: Nat)

Defined in Data.Nat

type (arg :: Nat) <= (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679392836Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg) arg1

type (arg :: Nat) < (arg1 :: Nat)

Defined in Data.Nat

type (arg :: Nat) < (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679392820Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg) arg1

type Compare (a1 :: Nat) (a2 :: Nat)

Defined in Data.Nat

type Compare (a1 :: Nat) (a2 :: Nat)

type (x :: Nat) /= (y :: Nat)

Defined in Data.Nat

type (x :: Nat) /= (y :: Nat) = Not (x == y)

type (a :: Nat) == (b :: Nat)

Defined in Data.Nat

type (a :: Nat) == (b :: Nat)

type ShowsPrec a1 (a2 :: Nat) a3

Defined in Data.Nat

type ShowsPrec a1 (a2 :: Nat) a3

type Apply LitSym0 (a6989586621679102719 :: Nat)

Defined in Data.Nat

type Apply LitSym0 (a6989586621679102719 :: Nat) = LitSym1 a6989586621679102719

type Apply SSym0 (a6989586621679056679 :: Nat)

Defined in Data.Nat

type Apply SSym0 (a6989586621679056679 :: Nat) = SSym1 a6989586621679056679

type family NatPlus a a where ...

Equations

NatPlus Z b = b

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

type family NatMul a a where ...

Equations

NatMul Z _ = ZSym0

NatMul (S a) b = Apply (Apply NatPlusSym0 b) (Apply (Apply NatMulSym0 a) b)

type family NatMinus a a where ...

Equations

NatMinus Z _ = ZSym0

NatMinus (S a) (S b) = Apply (Apply NatMinusSym0 a) b

NatMinus (S wild_6989586621679053208) Z = Let6989586621679056695ASym1 wild_6989586621679053208

type family NatAbs a where ...

Equations

NatAbs n = n

type family NatSignum a 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

data SNat :: Nat -> Type where

Constructors

SZ :: SNat (Z :: Nat)

SS :: forall (n :: Nat). (Sing n) -> SNat (S n :: Nat)

Instances

SDecide Nat => TestCoercion SNat

Defined in Data.Nat

Methods

testCoercion :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (Coercion a b)

SDecide Nat => TestEquality SNat

Defined in Data.Nat

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

Eq (SNat n)

Defined in Data.Nat

Methods

(==) :: SNat n -> SNat n -> Bool

(/=) :: SNat n -> SNat n -> Bool

Ord (SNat n)

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 (SNat z)

Defined in Data.Nat

Methods

showsPrec :: Int -> SNat z -> ShowS

show :: SNat z -> String

showList :: [SNat z] -> ShowS

type family Sing :: k -> Type

The singleton kind-indexed type family.

Instances

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SBool

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SOrdering

type Sing

Defined in Data.Singletons.TypeLits.Internal

type Sing = SNat

type Sing

Defined in Data.Singletons.TypeLits.Internal

type Sing = SSymbol

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple0

type Sing

Defined in Data.Nat

type Sing = SNat

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SVoid

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SAll

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SAny

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SList :: [a] -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SMaybe :: Maybe a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SMin :: Min a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SMax :: Max a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SFirst :: First a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SLast :: Last a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SWrappedMonoid :: WrappedMonoid m -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SOption :: Option a -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SIdentity :: Identity a -> Type

type Sing

Defined in Data.Singletons.Prelude.Monoid

type Sing = SFirst :: First a -> Type

type Sing

Defined in Data.Singletons.Prelude.Monoid

type Sing = SLast :: Last a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SDual :: Dual a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SSum :: Sum a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SProduct :: Product a -> Type

type Sing

Defined in Data.Singletons.Prelude.Ord

type Sing = SDown :: Down a -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SNonEmpty :: NonEmpty a -> Type

type Sing

Defined in Data.Singletons.Prelude.Foldable

type Sing = SEndo :: Endo a -> Type

type Sing

Defined in Data.Singletons.Prelude.Foldable

type Sing = SMaxInternal :: MaxInternal a -> Type

type Sing

Defined in Data.Singletons.Prelude.Foldable

type Sing = SMinInternal :: MinInternal a -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SEither :: Either a b -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple2 :: (a, b) -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup

type Sing = SArg :: Arg a b -> Type

type Sing

Defined in Data.Singletons.Prelude.Proxy

type Sing = SProxy :: Proxy t -> Type

type Sing

Defined in Data.Singletons.Internal

type Sing = SWrappedSing :: WrappedSing a -> Type

type Sing

Defined in Data.Singletons.Internal

type Sing = SLambda :: (k1 ~> k2) -> Type

type Sing

Defined in Data.Singletons.Prelude.Traversable

type Sing = SStateL :: StateL s a -> Type

type Sing

Defined in Data.Singletons.Prelude.Traversable

type Sing = SStateR :: StateR s a -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple3 :: (a, b, c) -> Type

type Sing

Defined in Data.Singletons.Prelude.Const

type Sing = SConst :: Const a b -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple4 :: (a, b, c, d) -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple5 :: (a, b, c, d, e) -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple6 :: (a, b, c, d, e, f) -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

class PNum a

Instances

PNum Nat

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

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)

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

Defined in Data.Singletons.Prelude.Num

Methods

(%+) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)

(%-) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2)

(%*) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)

sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t)

sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t)

sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t)

sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t)

SNum Nat

Defined in Data.Nat

Methods

(%+) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)

(%-) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2)

(%*) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)

sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t)

sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t)

sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t)

sFromInteger :: forall (t :: Nat0). Sing t -> Sing (Apply FromIntegerSym0 t)

SNum a => SNum (Down a)

Defined in Data.Singletons.Prelude.Num

Methods

(%+) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)

(%-) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2)

(%*) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)

sNegate :: forall (t :: Down a). Sing t -> Sing (Apply NegateSym0 t)

sAbs :: forall (t :: Down a). Sing t -> Sing (Apply AbsSym0 t)

sSignum :: forall (t :: Down a). Sing t -> Sing (Apply SignumSym0 t)

sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t)

data SSym0 a6989586621679056679 where

Constructors

SSym0KindInference :: SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0 a6989586621679056679

Instances

SuppressUnusedWarnings SSym0

Defined in Data.Nat

Methods

suppressUnusedWarnings :: ()

SingI SSym0

Defined in Data.Nat

Methods

sing :: Sing SSym0

type Apply SSym0 (a6989586621679056679 :: Nat)

Defined in Data.Nat

type Apply SSym0 (a6989586621679056679 :: Nat) = SSym1 a6989586621679056679

type SSym1 (a6989586621679056679 :: Nat) = S a6989586621679056679 :: Nat

type ZSym0 = Z :: Nat

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 a6989586621679102719 where

Constructors

LitSym0KindInference :: SameKind (Apply LitSym0 arg) (LitSym1 arg) => LitSym0 a6989586621679102719

Instances

SuppressUnusedWarnings LitSym0

Defined in Data.Nat

Methods

suppressUnusedWarnings :: ()

type Apply LitSym0 (a6989586621679102719 :: Nat)

Defined in Data.Nat

type Apply LitSym0 (a6989586621679102719 :: Nat) = LitSym1 a6989586621679102719

type LitSym1 (a6989586621679102719 :: Nat) = Lit a6989586621679102719 :: Nat

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))))