Copyright	(C) 2014 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Num

Contents

Defunctionalization symbols

Description

Defines and exports promoted and singleton versions of definitions from GHC.Num.

Be warned that some of the associated type families in the PNum class ((+), (-), and (*)) clash with their counterparts for Nat in the GHC.TypeLits module.

Synopsis

class PNum (a :: Type) where
- type (arg :: a) + (arg :: a) :: a
- type (arg :: a) - (arg :: a) :: a
- type (arg :: a) * (arg :: a) :: a
- type Negate (arg :: a) :: a
- type Abs (arg :: a) :: a
- type Signum (arg :: a) :: a
- type FromInteger (arg :: Nat) :: a
class SNum a where
- (%+) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t :: a)
- (%-) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t :: a)
- (%*) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t :: a)
- sNegate :: forall (t :: a). Sing t -> Sing (Apply NegateSym0 t :: a)
- sAbs :: forall (t :: a). Sing t -> Sing (Apply AbsSym0 t :: a)
- sSignum :: forall (t :: a). Sing t -> Sing (Apply SignumSym0 t :: a)
- sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t :: a)
type family Subtract (a :: a) (a :: a) :: a where ...
sSubtract :: forall a (t :: a) (t :: a). SNum a => Sing t -> Sing t -> Sing (Apply (Apply SubtractSym0 t) t :: a)
data (+@#@$) :: forall a6989586621679529343. (~>) a6989586621679529343 ((~>) a6989586621679529343 a6989586621679529343)
data (+@#@$$) (arg6989586621679529362 :: a6989586621679529343) :: (~>) a6989586621679529343 a6989586621679529343
type (+@#@$$$) (arg6989586621679529362 :: a6989586621679529343) (arg6989586621679529363 :: a6989586621679529343) = (+) arg6989586621679529362 arg6989586621679529363
data (-@#@$) :: forall a6989586621679529343. (~>) a6989586621679529343 ((~>) a6989586621679529343 a6989586621679529343)
data (-@#@$$) (arg6989586621679529366 :: a6989586621679529343) :: (~>) a6989586621679529343 a6989586621679529343
type (-@#@$$$) (arg6989586621679529366 :: a6989586621679529343) (arg6989586621679529367 :: a6989586621679529343) = (-) arg6989586621679529366 arg6989586621679529367
data (*@#@$) :: forall a6989586621679529343. (~>) a6989586621679529343 ((~>) a6989586621679529343 a6989586621679529343)
data (*@#@$$) (arg6989586621679529370 :: a6989586621679529343) :: (~>) a6989586621679529343 a6989586621679529343
type (*@#@$$$) (arg6989586621679529370 :: a6989586621679529343) (arg6989586621679529371 :: a6989586621679529343) = * arg6989586621679529370 arg6989586621679529371
data NegateSym0 :: forall a6989586621679529343. (~>) a6989586621679529343 a6989586621679529343
type NegateSym1 (arg6989586621679529374 :: a6989586621679529343) = Negate arg6989586621679529374
data AbsSym0 :: forall a6989586621679529343. (~>) a6989586621679529343 a6989586621679529343
type AbsSym1 (arg6989586621679529376 :: a6989586621679529343) = Abs arg6989586621679529376
data SignumSym0 :: forall a6989586621679529343. (~>) a6989586621679529343 a6989586621679529343
type SignumSym1 (arg6989586621679529378 :: a6989586621679529343) = Signum arg6989586621679529378
data FromIntegerSym0 :: forall a6989586621679529343. (~>) Nat a6989586621679529343
type FromIntegerSym1 (arg6989586621679529380 :: Nat) = FromInteger arg6989586621679529380
data SubtractSym0 :: forall a6989586621679535047. (~>) a6989586621679535047 ((~>) a6989586621679535047 a6989586621679535047)
data SubtractSym1 (a6989586621679535051 :: a6989586621679535047) :: (~>) a6989586621679535047 a6989586621679535047
type SubtractSym2 (a6989586621679535051 :: a6989586621679535047) (a6989586621679535052 :: a6989586621679535047) = Subtract a6989586621679535051 a6989586621679535052

Documentation

class PNum (a :: Type) Source #

Associated Types

type (arg :: a) + (arg :: a) :: a infixl 6 Source #

type (arg :: a) - (arg :: a) :: a infixl 6 Source #

type (-) a a = Apply (Apply TFHelper_6989586621679529384Sym0 a) a Source #

type (arg :: a) * (arg :: a) :: a infixl 7 Source #

type Negate (arg :: a) :: a Source #

type Negate a = Apply Negate_6989586621679529395Sym0 a Source #

type Abs (arg :: a) :: a Source #

type Signum (arg :: a) :: a Source #

type FromInteger (arg :: Nat) :: a Source #

Instances

Instances details

PNum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Num Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #
PNum (Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #
PNum (Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #
PNum (Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Identity Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #
PNum (Sum a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #
PNum (Product a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #
PNum (Down a) Source #
Instance details Defined in Data.Singletons.Prelude.Num Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #
PNum (Const a b) Source #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #

class SNum a where Source #

Minimal complete definition

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

Methods

(%+) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t :: a) infixl 6 Source #

(%-) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t :: a) infixl 6 Source #

default (%-) :: forall (t :: a) (t :: a). (Apply (Apply (-@#@$) t) t :: a) ~ Apply (Apply TFHelper_6989586621679529384Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t :: a) Source #

(%*) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t :: a) infixl 7 Source #

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

default sNegate :: forall (t :: a). (Apply NegateSym0 t :: a) ~ Apply Negate_6989586621679529395Sym0 t => Sing t -> Sing (Apply NegateSym0 t :: a) Source #

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

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

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

Instances

Instances details

SNum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods (%+) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) Source # sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #
SNum a => SNum (Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods (%+) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) Source # sNegate :: forall (t :: Min a). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Min a). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Min a). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #
SNum a => SNum (Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods (%+) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) Source # sNegate :: forall (t :: Max a). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Max a). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Max a). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #
SNum a => SNum (Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Identity Methods (%+) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) Source # sNegate :: forall (t :: Identity a). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Identity a). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Identity a). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #
SNum a => SNum (Sum a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%+) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) Source # sNegate :: forall (t :: Sum a). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Sum a). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Sum a). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #
SNum a => SNum (Product a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%+) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) Source # sNegate :: forall (t :: Product a). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Product a). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Product a). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #
SNum a => SNum (Down a) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods (%+) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) Source # sNegate :: forall (t :: Down a). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Down a). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Down a). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #
SNum a => SNum (Const a b) Source #
Instance details Defined in Data.Singletons.Prelude.Const Methods (%+) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source # (%-) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source # (%) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) Source # sNegate :: forall (t :: Const a b). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Const a b). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Const a b). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #

type family Subtract (a :: a) (a :: a) :: a where ... Source #

Equations

Subtract x y = Apply (Apply (-@#@$) y) x

sSubtract :: forall a (t :: a) (t :: a). SNum a => Sing t -> Sing t -> Sing (Apply (Apply SubtractSym0 t) t :: a) Source #

Defunctionalization symbols

data (+@#@$) :: forall a6989586621679529343. (~>) a6989586621679529343 ((~>) a6989586621679529343 a6989586621679529343) infixl 6 Source #

Instances

Instances details

SNum a => SingI ((+@#@$) :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (+@#@$) Source #
SuppressUnusedWarnings ((+@#@$) :: TyFun a6989586621679529343 (a6989586621679529343 ~> a6989586621679529343) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((+@#@$) :: TyFun a6989586621679529343 (a6989586621679529343 ~> a6989586621679529343) -> Type) (arg6989586621679529362 :: a6989586621679529343) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((+@#@$) :: TyFun a6989586621679529343 (a6989586621679529343 ~> a6989586621679529343) -> Type) (arg6989586621679529362 :: a6989586621679529343) = (+@#@$$) arg6989586621679529362

data (+@#@$$) (arg6989586621679529362 :: a6989586621679529343) :: (~>) a6989586621679529343 a6989586621679529343 infixl 6 Source #

Instances

Instances details

(SNum a, SingI d) => SingI ((+@#@$$) d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing ((+@#@$$) d) Source #
SuppressUnusedWarnings ((+@#@$$) arg6989586621679529362 :: TyFun a6989586621679529343 a6989586621679529343 -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((+@#@$$) arg6989586621679529362 :: TyFun a a -> Type) (arg6989586621679529363 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((+@#@$$) arg6989586621679529362 :: TyFun a a -> Type) (arg6989586621679529363 :: a) = arg6989586621679529362 + arg6989586621679529363

type (+@#@$$$) (arg6989586621679529362 :: a6989586621679529343) (arg6989586621679529363 :: a6989586621679529343) = (+) arg6989586621679529362 arg6989586621679529363 Source #

data (-@#@$) :: forall a6989586621679529343. (~>) a6989586621679529343 ((~>) a6989586621679529343 a6989586621679529343) infixl 6 Source #

Instances

Instances details

SNum a => SingI ((-@#@$) :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (-@#@$) Source #
SuppressUnusedWarnings ((-@#@$) :: TyFun a6989586621679529343 (a6989586621679529343 ~> a6989586621679529343) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((-@#@$) :: TyFun a6989586621679529343 (a6989586621679529343 ~> a6989586621679529343) -> Type) (arg6989586621679529366 :: a6989586621679529343) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((-@#@$) :: TyFun a6989586621679529343 (a6989586621679529343 ~> a6989586621679529343) -> Type) (arg6989586621679529366 :: a6989586621679529343) = (-@#@$$) arg6989586621679529366

data (-@#@$$) (arg6989586621679529366 :: a6989586621679529343) :: (~>) a6989586621679529343 a6989586621679529343 infixl 6 Source #

Instances

Instances details

(SNum a, SingI d) => SingI ((-@#@$$) d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing ((-@#@$$) d) Source #
SuppressUnusedWarnings ((-@#@$$) arg6989586621679529366 :: TyFun a6989586621679529343 a6989586621679529343 -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((-@#@$$) arg6989586621679529366 :: TyFun a a -> Type) (arg6989586621679529367 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((-@#@$$) arg6989586621679529366 :: TyFun a a -> Type) (arg6989586621679529367 :: a) = arg6989586621679529366 - arg6989586621679529367

type (-@#@$$$) (arg6989586621679529366 :: a6989586621679529343) (arg6989586621679529367 :: a6989586621679529343) = (-) arg6989586621679529366 arg6989586621679529367 Source #

data (*@#@$) :: forall a6989586621679529343. (~>) a6989586621679529343 ((~>) a6989586621679529343 a6989586621679529343) infixl 7 Source #

Instances

Instances details

SNum a => SingI ((*@#@$) :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (*@#@$) Source #
SuppressUnusedWarnings ((*@#@$) :: TyFun a6989586621679529343 (a6989586621679529343 ~> a6989586621679529343) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((*@#@$) :: TyFun a6989586621679529343 (a6989586621679529343 ~> a6989586621679529343) -> Type) (arg6989586621679529370 :: a6989586621679529343) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$) :: TyFun a6989586621679529343 (a6989586621679529343 ~> a6989586621679529343) -> Type) (arg6989586621679529370 :: a6989586621679529343) = (@#@$$) arg6989586621679529370

data (*@#@$$) (arg6989586621679529370 :: a6989586621679529343) :: (~>) a6989586621679529343 a6989586621679529343 infixl 7 Source #

Instances

Instances details

(SNum a, SingI d) => SingI ((*@#@$$) d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing ((*@#@$$) d) Source #
SuppressUnusedWarnings ((*@#@$$) arg6989586621679529370 :: TyFun a6989586621679529343 a6989586621679529343 -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((*@#@$$) arg6989586621679529370 :: TyFun a a -> Type) (arg6989586621679529371 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$$) arg6989586621679529370 :: TyFun a a -> Type) (arg6989586621679529371 :: a) = arg6989586621679529370 arg6989586621679529371

type (*@#@$$$) (arg6989586621679529370 :: a6989586621679529343) (arg6989586621679529371 :: a6989586621679529343) = * arg6989586621679529370 arg6989586621679529371 Source #

data NegateSym0 :: forall a6989586621679529343. (~>) a6989586621679529343 a6989586621679529343 Source #

Instances

Instances details

SNum a => SingI (NegateSym0 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing NegateSym0 Source #
SuppressUnusedWarnings (NegateSym0 :: TyFun a6989586621679529343 a6989586621679529343 -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (NegateSym0 :: TyFun a a -> Type) (arg6989586621679529374 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (NegateSym0 :: TyFun a a -> Type) (arg6989586621679529374 :: a) = Negate arg6989586621679529374

type NegateSym1 (arg6989586621679529374 :: a6989586621679529343) = Negate arg6989586621679529374 Source #

data AbsSym0 :: forall a6989586621679529343. (~>) a6989586621679529343 a6989586621679529343 Source #

Instances

Instances details

SNum a => SingI (AbsSym0 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing AbsSym0 Source #
SuppressUnusedWarnings (AbsSym0 :: TyFun a6989586621679529343 a6989586621679529343 -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (AbsSym0 :: TyFun a a -> Type) (arg6989586621679529376 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (AbsSym0 :: TyFun a a -> Type) (arg6989586621679529376 :: a) = Abs arg6989586621679529376

type AbsSym1 (arg6989586621679529376 :: a6989586621679529343) = Abs arg6989586621679529376 Source #

data SignumSym0 :: forall a6989586621679529343. (~>) a6989586621679529343 a6989586621679529343 Source #

Instances

Instances details

SNum a => SingI (SignumSym0 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing SignumSym0 Source #
SuppressUnusedWarnings (SignumSym0 :: TyFun a6989586621679529343 a6989586621679529343 -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (SignumSym0 :: TyFun a a -> Type) (arg6989586621679529378 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SignumSym0 :: TyFun a a -> Type) (arg6989586621679529378 :: a) = Signum arg6989586621679529378

type SignumSym1 (arg6989586621679529378 :: a6989586621679529343) = Signum arg6989586621679529378 Source #

data FromIntegerSym0 :: forall a6989586621679529343. (~>) Nat a6989586621679529343 Source #

Instances

Instances details

SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing FromIntegerSym0 Source #
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679529343 -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679529380 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679529380 :: Nat) = FromInteger arg6989586621679529380 :: k2

type FromIntegerSym1 (arg6989586621679529380 :: Nat) = FromInteger arg6989586621679529380 Source #

data SubtractSym0 :: forall a6989586621679535047. (~>) a6989586621679535047 ((~>) a6989586621679535047 a6989586621679535047) Source #

Instances

Instances details

SNum a => SingI (SubtractSym0 :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing SubtractSym0 Source #
SuppressUnusedWarnings (SubtractSym0 :: TyFun a6989586621679535047 (a6989586621679535047 ~> a6989586621679535047) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (SubtractSym0 :: TyFun a6989586621679535047 (a6989586621679535047 ~> a6989586621679535047) -> Type) (a6989586621679535051 :: a6989586621679535047) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SubtractSym0 :: TyFun a6989586621679535047 (a6989586621679535047 ~> a6989586621679535047) -> Type) (a6989586621679535051 :: a6989586621679535047) = SubtractSym1 a6989586621679535051

data SubtractSym1 (a6989586621679535051 :: a6989586621679535047) :: (~>) a6989586621679535047 a6989586621679535047 Source #

Instances

Instances details

(SNum a, SingI d) => SingI (SubtractSym1 d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (SubtractSym1 d) Source #
SuppressUnusedWarnings (SubtractSym1 a6989586621679535051 :: TyFun a6989586621679535047 a6989586621679535047 -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (SubtractSym1 a6989586621679535051 :: TyFun a a -> Type) (a6989586621679535052 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SubtractSym1 a6989586621679535051 :: TyFun a a -> Type) (a6989586621679535052 :: a) = Subtract a6989586621679535051 a6989586621679535052

type SubtractSym2 (a6989586621679535051 :: a6989586621679535047) (a6989586621679535052 :: a6989586621679535047) = Subtract a6989586621679535051 a6989586621679535052 Source #