singletons-2.6: A framework for generating singleton types

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 a6989586621679525469. (~>) a6989586621679525469 ((~>) a6989586621679525469 a6989586621679525469)
- data (+@#@$$) (arg6989586621679525488 :: a6989586621679525469) :: (~>) a6989586621679525469 a6989586621679525469
- type (+@#@$$$) (arg6989586621679525488 :: a6989586621679525469) (arg6989586621679525489 :: a6989586621679525469) = (+) arg6989586621679525488 arg6989586621679525489
- data (-@#@$) :: forall a6989586621679525469. (~>) a6989586621679525469 ((~>) a6989586621679525469 a6989586621679525469)
- data (-@#@$$) (arg6989586621679525492 :: a6989586621679525469) :: (~>) a6989586621679525469 a6989586621679525469
- type (-@#@$$$) (arg6989586621679525492 :: a6989586621679525469) (arg6989586621679525493 :: a6989586621679525469) = (-) arg6989586621679525492 arg6989586621679525493
- data (*@#@$) :: forall a6989586621679525469. (~>) a6989586621679525469 ((~>) a6989586621679525469 a6989586621679525469)
- data (*@#@$$) (arg6989586621679525496 :: a6989586621679525469) :: (~>) a6989586621679525469 a6989586621679525469
- type (*@#@$$$) (arg6989586621679525496 :: a6989586621679525469) (arg6989586621679525497 :: a6989586621679525469) = * arg6989586621679525496 arg6989586621679525497
- data NegateSym0 :: forall a6989586621679525469. (~>) a6989586621679525469 a6989586621679525469
- type NegateSym1 (arg6989586621679525500 :: a6989586621679525469) = Negate arg6989586621679525500
- data AbsSym0 :: forall a6989586621679525469. (~>) a6989586621679525469 a6989586621679525469
- type AbsSym1 (arg6989586621679525502 :: a6989586621679525469) = Abs arg6989586621679525502
- data SignumSym0 :: forall a6989586621679525469. (~>) a6989586621679525469 a6989586621679525469
- type SignumSym1 (arg6989586621679525504 :: a6989586621679525469) = Signum arg6989586621679525504
- data FromIntegerSym0 :: forall a6989586621679525469. (~>) Nat a6989586621679525469
- type FromIntegerSym1 (arg6989586621679525506 :: Nat) = FromInteger arg6989586621679525506
- data SubtractSym0 :: forall a6989586621679531173. (~>) a6989586621679531173 ((~>) a6989586621679531173 a6989586621679531173)
- data SubtractSym1 (a6989586621679531177 :: a6989586621679531173) :: (~>) a6989586621679531173 a6989586621679531173
- type SubtractSym2 (a6989586621679531177 :: a6989586621679531173) (a6989586621679531178 :: a6989586621679531173) = Subtract a6989586621679531177 a6989586621679531178

# 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_6989586621679525510Sym0 a) a Source #

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

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

type Negate a = Apply Negate_6989586621679525521Sym0 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 (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 (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 (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 (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 (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 (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 (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_6989586621679525510Sym0 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_6989586621679525521Sym0 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 (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 (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 (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 (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 (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 (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 (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 a6989586621679525469. (~>) a6989586621679525469 ((~>) a6989586621679525469 a6989586621679525469) 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 a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((+@#@$) :: TyFun a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) (arg6989586621679525488 :: a6989586621679525469) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((+@#@$) :: TyFun a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) (arg6989586621679525488 :: a6989586621679525469) = (+@#@$$) arg6989586621679525488

data (+@#@$$) (arg6989586621679525488 :: a6989586621679525469) :: (~>) a6989586621679525469 a6989586621679525469 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 ((+@#@$$) arg6989586621679525488 :: TyFun a6989586621679525469 a6989586621679525469 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((+@#@$$) arg6989586621679525488 :: TyFun a a -> Type) (arg6989586621679525489 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((+@#@$$) arg6989586621679525488 :: TyFun a a -> Type) (arg6989586621679525489 :: a) = arg6989586621679525488 + arg6989586621679525489

type (+@#@$$$) (arg6989586621679525488 :: a6989586621679525469) (arg6989586621679525489 :: a6989586621679525469) = (+) arg6989586621679525488 arg6989586621679525489 Source #

data (-@#@$) :: forall a6989586621679525469. (~>) a6989586621679525469 ((~>) a6989586621679525469 a6989586621679525469) 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 a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((-@#@$) :: TyFun a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) (arg6989586621679525492 :: a6989586621679525469) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((-@#@$) :: TyFun a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) (arg6989586621679525492 :: a6989586621679525469) = (-@#@$$) arg6989586621679525492

data (-@#@$$) (arg6989586621679525492 :: a6989586621679525469) :: (~>) a6989586621679525469 a6989586621679525469 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 ((-@#@$$) arg6989586621679525492 :: TyFun a6989586621679525469 a6989586621679525469 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((-@#@$$) arg6989586621679525492 :: TyFun a a -> Type) (arg6989586621679525493 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((-@#@$$) arg6989586621679525492 :: TyFun a a -> Type) (arg6989586621679525493 :: a) = arg6989586621679525492 - arg6989586621679525493

type (-@#@$$$) (arg6989586621679525492 :: a6989586621679525469) (arg6989586621679525493 :: a6989586621679525469) = (-) arg6989586621679525492 arg6989586621679525493 Source #

data (*@#@$) :: forall a6989586621679525469. (~>) a6989586621679525469 ((~>) a6989586621679525469 a6989586621679525469) 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 a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((*@#@$) :: TyFun a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) (arg6989586621679525496 :: a6989586621679525469) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((*@#@$) :: TyFun a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) (arg6989586621679525496 :: a6989586621679525469) = (*@#@$$) arg6989586621679525496

data (*@#@$$) (arg6989586621679525496 :: a6989586621679525469) :: (~>) a6989586621679525469 a6989586621679525469 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 ((*@#@$$) arg6989586621679525496 :: TyFun a6989586621679525469 a6989586621679525469 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((*@#@$$) arg6989586621679525496 :: TyFun a a -> Type) (arg6989586621679525497 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((*@#@$$) arg6989586621679525496 :: TyFun a a -> Type) (arg6989586621679525497 :: a) = arg6989586621679525496 * arg6989586621679525497

type (*@#@$$$) (arg6989586621679525496 :: a6989586621679525469) (arg6989586621679525497 :: a6989586621679525469) = * arg6989586621679525496 arg6989586621679525497 Source #

data NegateSym0 :: forall a6989586621679525469. (~>) a6989586621679525469 a6989586621679525469 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 a6989586621679525469 a6989586621679525469 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (NegateSym0 :: TyFun a a -> Type) (arg6989586621679525500 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply (NegateSym0 :: TyFun a a -> Type) (arg6989586621679525500 :: a) = Negate arg6989586621679525500

type NegateSym1 (arg6989586621679525500 :: a6989586621679525469) = Negate arg6989586621679525500 Source #

data AbsSym0 :: forall a6989586621679525469. (~>) a6989586621679525469 a6989586621679525469 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 a6989586621679525469 a6989586621679525469 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (AbsSym0 :: TyFun a a -> Type) (arg6989586621679525502 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply (AbsSym0 :: TyFun a a -> Type) (arg6989586621679525502 :: a) = Abs arg6989586621679525502

type AbsSym1 (arg6989586621679525502 :: a6989586621679525469) = Abs arg6989586621679525502 Source #

data SignumSym0 :: forall a6989586621679525469. (~>) a6989586621679525469 a6989586621679525469 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 a6989586621679525469 a6989586621679525469 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (SignumSym0 :: TyFun a a -> Type) (arg6989586621679525504 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SignumSym0 :: TyFun a a -> Type) (arg6989586621679525504 :: a) = Signum arg6989586621679525504

type SignumSym1 (arg6989586621679525504 :: a6989586621679525469) = Signum arg6989586621679525504 Source #

data FromIntegerSym0 :: forall a6989586621679525469. (~>) Nat a6989586621679525469 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 a6989586621679525469 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679525506 :: Nat) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (arg6989586621679525506 :: Nat) = FromInteger arg6989586621679525506 :: k2

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

data SubtractSym0 :: forall a6989586621679531173. (~>) a6989586621679531173 ((~>) a6989586621679531173 a6989586621679531173) 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 a6989586621679531173 (a6989586621679531173 ~> a6989586621679531173) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (SubtractSym0 :: TyFun a6989586621679531173 (a6989586621679531173 ~> a6989586621679531173) -> Type) (a6989586621679531177 :: a6989586621679531173) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SubtractSym0 :: TyFun a6989586621679531173 (a6989586621679531173 ~> a6989586621679531173) -> Type) (a6989586621679531177 :: a6989586621679531173) = SubtractSym1 a6989586621679531177

data SubtractSym1 (a6989586621679531177 :: a6989586621679531173) :: (~>) a6989586621679531173 a6989586621679531173 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 a6989586621679531177 :: TyFun a6989586621679531173 a6989586621679531173 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (SubtractSym1 a6989586621679531177 :: TyFun a a -> Type) (a6989586621679531178 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SubtractSym1 a6989586621679531177 :: TyFun a a -> Type) (a6989586621679531178 :: a) = Subtract a6989586621679531177 a6989586621679531178

type SubtractSym2 (a6989586621679531177 :: a6989586621679531173) (a6989586621679531178 :: a6989586621679531173) = Subtract a6989586621679531177 a6989586621679531178 Source #