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

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

(%+) :: 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

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

Defined in Data.Nat

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b)

(%/=) :: 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

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SingKind Nat

Defined in Data.Nat

Associated Types

type Demote Nat = (r :: Type)

Methods

fromSing :: Sing a -> Demote Nat

toSing :: Demote Nat -> SomeSing Nat

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)

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

Defined in Data.Nat

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

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

SingI (TyCon1 S)

Defined in Data.Nat

Methods

sing :: Sing (TyCon1 S)

data Sing (a :: Nat)

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

Defined in Data.Nat

type Demote Nat = Nat

type Show_ (arg :: Nat)

Defined in Data.Nat

type Show_ (arg :: Nat) = Apply (Show__6989586621680262717Sym0 :: 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_6989586621679505486Sym0 :: TyFun Nat Nat -> Type) arg

type ShowList (arg :: [Nat]) arg1

Defined in Data.Nat

type ShowList (arg :: [Nat]) arg1 = Apply (Apply (ShowList_6989586621680262728Sym0 :: 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_6989586621679380222Sym0 :: 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_6989586621679380204Sym0 :: TyFun Nat (Nat ~> Nat) -> Type) arg) arg1

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

Defined in Data.Nat

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

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

Defined in Data.Nat

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

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

Defined in Data.Nat

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

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

Defined in Data.Nat

type (arg :: Nat) < (arg1 :: Nat) = Apply (Apply (TFHelper_6989586621679380132Sym0 :: 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 (n6989586621679094994 :: Nat)

Defined in Data.Nat

type Apply LitSym0 (n6989586621679094994 :: Nat) = Lit n6989586621679094994

type Apply SSym0 (t6989586621679080960 :: Nat)

Defined in Data.Nat

type Apply SSym0 (t6989586621679080960 :: Nat) = S t6989586621679080960

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)

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

Defined in Data.Nat

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

data Sing (a :: Bool)

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)

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)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: forall (n :: Nat). KnownNat n => Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: forall (n :: Symbol). KnownSymbol n => Sing n

data Sing (a :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

• STuple0 :: forall (a :: ()). Sing ()

data Sing (a :: Nat)

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)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)

data Sing (a :: All)

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)

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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 :: MaxInternal a)

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 (b :: MinInternal a)

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 (c :: Either a b)

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

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)

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)

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)

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)

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

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)

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

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

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

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

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

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

(%+) :: 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

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)

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 t6989586621679080960 arg. SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0 t6989586621679080960

Instances

SuppressUnusedWarnings SSym0

Defined in Data.Nat

Methods

suppressUnusedWarnings :: ()

SingI SSym0

Defined in Data.Nat

Methods

sing :: Sing SSym0

type Apply SSym0 (t6989586621679080960 :: Nat)

Defined in Data.Nat

type Apply SSym0 (t6989586621679080960 :: Nat) = S t6989586621679080960

type SSym1 (t6989586621679080960 :: Nat) = S t6989586621679080960

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 n6989586621679094994 arg. SameKind (Apply LitSym0 arg) (LitSym1 arg) => LitSym0 n6989586621679094994

Instances

SuppressUnusedWarnings LitSym0

Defined in Data.Nat

Methods

suppressUnusedWarnings :: ()

type Apply LitSym0 (n6989586621679094994 :: Nat)

Defined in Data.Nat

type Apply LitSym0 (n6989586621679094994 :: Nat) = Lit n6989586621679094994

type LitSym1 (n6989586621679094994 :: Nat) = Lit n6989586621679094994

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