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 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 where ...
sSubtract :: forall a (t :: a) (t :: a). SNum a => Sing t -> Sing t -> Sing (Apply (Apply SubtractSym0 t) t :: a)
data (+@#@$) a6989586621679517796
data a6989586621679517796 +@#@$$ a6989586621679517797
type (+@#@$$$) (a6989586621679517796 :: a) (a6989586621679517797 :: a) = (+) a6989586621679517796 a6989586621679517797 :: a
data (-@#@$) a6989586621679517801
data a6989586621679517801 -@#@$$ a6989586621679517802
type (-@#@$$$) (a6989586621679517801 :: a) (a6989586621679517802 :: a) = (-) a6989586621679517801 a6989586621679517802 :: a
data (*@#@$) a6989586621679517806
data a6989586621679517806 *@#@$$ a6989586621679517807
type (*@#@$$$) (a6989586621679517806 :: a) (a6989586621679517807 :: a) = * a6989586621679517806 a6989586621679517807 :: a
data NegateSym0 a6989586621679517810
type NegateSym1 (a6989586621679517810 :: a) = Negate a6989586621679517810 :: a
data AbsSym0 a6989586621679517813
type AbsSym1 (a6989586621679517813 :: a) = Abs a6989586621679517813 :: a
data SignumSym0 a6989586621679517816
type SignumSym1 (a6989586621679517816 :: a) = Signum a6989586621679517816 :: a
data FromIntegerSym0 a6989586621679517819
type FromIntegerSym1 (a6989586621679517819 :: Nat) = FromInteger a6989586621679517819 :: a
data SubtractSym0 a6989586621679517789
data SubtractSym1 a6989586621679517789 a6989586621679517790
type SubtractSym2 (a6989586621679517789 :: a) (a6989586621679517790 :: a) = Subtract a6989586621679517789 a6989586621679517790 :: a

Documentation

class PNum a 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_6989586621679517822Sym0 a) a

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

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

type Negate a = Apply Negate_6989586621679517832Sym0 a

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

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

type (+@#@$$$) (a6989586621679517796 :: a) (a6989586621679517797 :: a) = (+) a6989586621679517796 a6989586621679517797 :: a infixl 6 Source #

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

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

type (-@#@$$$) (a6989586621679517801 :: a) (a6989586621679517802 :: a) = (-) a6989586621679517801 a6989586621679517802 :: a infixl 6 Source #

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

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

type (*@#@$$$) (a6989586621679517806 :: a) (a6989586621679517807 :: a) = * a6989586621679517806 a6989586621679517807 :: a infixl 7 Source #

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

type NegateSym1 (a6989586621679517810 :: a) = Negate a6989586621679517810 :: a Source #

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

type AbsSym1 (a6989586621679517813 :: a) = Abs a6989586621679517813 :: a Source #

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

type SignumSym1 (a6989586621679517816 :: a) = Signum a6989586621679517816 :: a Source #

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

type FromIntegerSym1 (a6989586621679517819 :: Nat) = FromInteger a6989586621679517819 :: a Source #

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

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

type SubtractSym2 (a6989586621679517789 :: a) (a6989586621679517790 :: a) = Subtract a6989586621679517789 a6989586621679517790 :: a Source #