singletons-2.6: A framework for generating singleton types
Copyright(C) 2014 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRyan Scott
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Prelude.Num

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

SuppressUnusedWarnings ((+@#@$) :: TyFun a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

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

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

SuppressUnusedWarnings ((-@#@$) :: TyFun a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

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

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

SuppressUnusedWarnings ((*@#@$) :: TyFun a6989586621679525469 (a6989586621679525469 ~> a6989586621679525469) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

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

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

SuppressUnusedWarnings (NegateSym0 :: TyFun a6989586621679525469 a6989586621679525469 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

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

SuppressUnusedWarnings (AbsSym0 :: TyFun a6989586621679525469 a6989586621679525469 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

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

SuppressUnusedWarnings (SignumSym0 :: TyFun a6989586621679525469 a6989586621679525469 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

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

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679525469 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

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

SuppressUnusedWarnings (SubtractSym0 :: TyFun a6989586621679531173 (a6989586621679531173 ~> a6989586621679531173) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Num

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

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 #