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 a6989586621679523498. (~>) a6989586621679523498 ((~>) a6989586621679523498 a6989586621679523498)
data (+@#@$$) (arg6989586621679523518 :: a6989586621679523498) :: (~>) a6989586621679523498 a6989586621679523498
type (+@#@$$$) (arg6989586621679523518 :: a6989586621679523498) (arg6989586621679523519 :: a6989586621679523498) = (+) arg6989586621679523518 arg6989586621679523519
data (-@#@$) :: forall a6989586621679523498. (~>) a6989586621679523498 ((~>) a6989586621679523498 a6989586621679523498)
data (-@#@$$) (arg6989586621679523522 :: a6989586621679523498) :: (~>) a6989586621679523498 a6989586621679523498
type (-@#@$$$) (arg6989586621679523522 :: a6989586621679523498) (arg6989586621679523523 :: a6989586621679523498) = (-) arg6989586621679523522 arg6989586621679523523
data (*@#@$) :: forall a6989586621679523498. (~>) a6989586621679523498 ((~>) a6989586621679523498 a6989586621679523498)
data (*@#@$$) (arg6989586621679523526 :: a6989586621679523498) :: (~>) a6989586621679523498 a6989586621679523498
type (*@#@$$$) (arg6989586621679523526 :: a6989586621679523498) (arg6989586621679523527 :: a6989586621679523498) = * arg6989586621679523526 arg6989586621679523527
data NegateSym0 :: forall a6989586621679523498. (~>) a6989586621679523498 a6989586621679523498
type NegateSym1 (arg6989586621679523530 :: a6989586621679523498) = Negate arg6989586621679523530
data AbsSym0 :: forall a6989586621679523498. (~>) a6989586621679523498 a6989586621679523498
type AbsSym1 (arg6989586621679523532 :: a6989586621679523498) = Abs arg6989586621679523532
data SignumSym0 :: forall a6989586621679523498. (~>) a6989586621679523498 a6989586621679523498
type SignumSym1 (arg6989586621679523534 :: a6989586621679523498) = Signum arg6989586621679523534
data FromIntegerSym0 :: forall a6989586621679523498. (~>) Nat a6989586621679523498
type FromIntegerSym1 (arg6989586621679523536 :: Nat) = FromInteger arg6989586621679523536
data SubtractSym0 :: forall a6989586621679528955. (~>) a6989586621679528955 ((~>) a6989586621679528955 a6989586621679528955)
data SubtractSym1 (a6989586621679528959 :: a6989586621679528955) :: (~>) a6989586621679528955 a6989586621679528955
type SubtractSym2 (a6989586621679528959 :: a6989586621679528955) (a6989586621679528960 :: a6989586621679528955) = Subtract a6989586621679528959 a6989586621679528960

Documentation

class PNum (a :: Type) #

Associated Types

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

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

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

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

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

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

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

Instances

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

class SNum a where #

Minimal complete definition

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

Methods

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

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

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

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

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

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

Instances

SNum Nat #
Instance details Defined in Data.Singletons.Prelude.Num Methods (%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) # (%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) # (%) :: Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) # 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 (Min a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods (%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) # (%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) # (%) :: Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) # 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 (Max a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods (%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) # (%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) # (%) :: Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) # 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 (Identity a) #
Instance details Defined in Data.Singletons.Prelude.Identity Methods (%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) # (%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) # (%) :: Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) # 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 (Sum a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) # (%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) # (%) :: Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) # 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 (Product a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) # (%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) # (%) :: Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) # 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) #
Instance details Defined in Data.Singletons.Prelude.Num Methods (%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) # (%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) # (%) :: Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) # 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 (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods (%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) # (%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) # (%) :: Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) # 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) #

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

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

Defunctionalization symbols

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

Instances

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

data (+@#@$$) (arg6989586621679523518 :: a6989586621679523498) :: (~>) a6989586621679523498 a6989586621679523498 infixl 6 #

Instances

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

type (+@#@$$$) (arg6989586621679523518 :: a6989586621679523498) (arg6989586621679523519 :: a6989586621679523498) = (+) arg6989586621679523518 arg6989586621679523519 #

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

Instances

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

data (-@#@$$) (arg6989586621679523522 :: a6989586621679523498) :: (~>) a6989586621679523498 a6989586621679523498 infixl 6 #

Instances

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

type (-@#@$$$) (arg6989586621679523522 :: a6989586621679523498) (arg6989586621679523523 :: a6989586621679523498) = (-) arg6989586621679523522 arg6989586621679523523 #

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

Instances

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

data (*@#@$$) (arg6989586621679523526 :: a6989586621679523498) :: (~>) a6989586621679523498 a6989586621679523498 infixl 7 #

Instances

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

type (*@#@$$$) (arg6989586621679523526 :: a6989586621679523498) (arg6989586621679523527 :: a6989586621679523498) = * arg6989586621679523526 arg6989586621679523527 #

data NegateSym0 :: forall a6989586621679523498. (~>) a6989586621679523498 a6989586621679523498 #

Instances

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

type NegateSym1 (arg6989586621679523530 :: a6989586621679523498) = Negate arg6989586621679523530 #

data AbsSym0 :: forall a6989586621679523498. (~>) a6989586621679523498 a6989586621679523498 #

Instances

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

type AbsSym1 (arg6989586621679523532 :: a6989586621679523498) = Abs arg6989586621679523532 #

data SignumSym0 :: forall a6989586621679523498. (~>) a6989586621679523498 a6989586621679523498 #

Instances

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

type SignumSym1 (arg6989586621679523534 :: a6989586621679523498) = Signum arg6989586621679523534 #

data FromIntegerSym0 :: forall a6989586621679523498. (~>) Nat a6989586621679523498 #

Instances

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

type FromIntegerSym1 (arg6989586621679523536 :: Nat) = FromInteger arg6989586621679523536 #

data SubtractSym0 :: forall a6989586621679528955. (~>) a6989586621679528955 ((~>) a6989586621679528955 a6989586621679528955) #

Instances

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

data SubtractSym1 (a6989586621679528959 :: a6989586621679528955) :: (~>) a6989586621679528955 a6989586621679528955 #

Instances

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

type SubtractSym2 (a6989586621679528959 :: a6989586621679528955) (a6989586621679528960 :: a6989586621679528955) = Subtract a6989586621679528959 a6989586621679528960 #