Data.Singletons.Prelude.Num

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.

Documentation

class PNum a

Associated Types

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

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

type a - a = Apply (Apply TFHelper_6989586621679517822Sym0 a) a

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

type Negate (arg :: a) :: a

type Negate a = Apply Negate_6989586621679517832Sym0 a

type Abs (arg :: a) :: a

type Signum (arg :: a) :: a

type FromInteger (arg :: Nat) :: a

Instances

PNum Nat

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)

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)

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)

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)

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)

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)

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)

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

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)

(%*) :: 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)

default sNegate :: forall (t :: a). (Apply NegateSym0 t :: a) ~ Apply Negate_6989586621679517832Sym0 t => 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)

Instances

SNum Nat

Defined in Data.Singletons.Prelude.Num

Methods

(%+) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t)

(%-) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t)

(%*) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t)

sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t)

sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t)

sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t)

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

SNum a => SNum (Min a)

Defined in Data.Singletons.Prelude.Semigroup

Methods

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

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

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

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

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

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

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

SNum a => SNum (Max a)

Defined in Data.Singletons.Prelude.Semigroup

Methods

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

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

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

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

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

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

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

SNum a => SNum (Identity a)

Defined in Data.Singletons.Prelude.Identity

Methods

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

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

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

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

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

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

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

SNum a => SNum (Sum a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

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

SNum a => SNum (Product a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

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

SNum a => SNum (Down a)

Defined in Data.Singletons.Prelude.Num

Methods

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

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

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

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

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

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

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

SNum a => SNum (Const a b)

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)

(%-) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t)

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

sNegate :: forall (t :: Const a b). Sing t -> Sing (Apply NegateSym0 t)

sAbs :: forall (t :: Const a b). Sing t -> Sing (Apply AbsSym0 t)

sSignum :: forall (t :: Const a b). Sing t -> Sing (Apply SignumSym0 t)

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

type family Subtract 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 (+@#@$) a6989586621679517796 infixl 6

Instances

SNum a => SingI ((+@#@$) :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (+@#@$)

SuppressUnusedWarnings ((+@#@$) :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((+@#@$) :: TyFun a (a ~> a) -> Type) (a6989586621679517796 :: a)

Defined in Data.Singletons.Prelude.Num

type Apply ((+@#@$) :: TyFun a (a ~> a) -> Type) (a6989586621679517796 :: a) = (+@#@$$) a6989586621679517796

data a6989586621679517796 +@#@$$ a6989586621679517797 infixl 6

Instances

(SNum a, SingI d) => SingI ((+@#@$$) d :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((+@#@$$) d)

SuppressUnusedWarnings ((+@#@$$) a6989586621679517796 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((+@#@$$) a6989586621679517796 :: TyFun a a -> Type) (a6989586621679517797 :: a)

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

data (-@#@$) a6989586621679517801 infixl 6

Instances

SNum a => SingI ((-@#@$) :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (-@#@$)

SuppressUnusedWarnings ((-@#@$) :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((-@#@$) :: TyFun a (a ~> a) -> Type) (a6989586621679517801 :: a)

Defined in Data.Singletons.Prelude.Num

type Apply ((-@#@$) :: TyFun a (a ~> a) -> Type) (a6989586621679517801 :: a) = (-@#@$$) a6989586621679517801

data a6989586621679517801 -@#@$$ a6989586621679517802 infixl 6

Instances

(SNum a, SingI d) => SingI ((-@#@$$) d :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((-@#@$$) d)

SuppressUnusedWarnings ((-@#@$$) a6989586621679517801 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((-@#@$$) a6989586621679517801 :: TyFun a a -> Type) (a6989586621679517802 :: a)

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

data (*@#@$) a6989586621679517806 infixl 7

Instances

SNum a => SingI ((*@#@$) :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (*@#@$)

SuppressUnusedWarnings ((*@#@$) :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((*@#@$) :: TyFun a (a ~> a) -> Type) (a6989586621679517806 :: a)

Defined in Data.Singletons.Prelude.Num

type Apply ((*@#@$) :: TyFun a (a ~> a) -> Type) (a6989586621679517806 :: a) = (*@#@$$) a6989586621679517806

data a6989586621679517806 *@#@$$ a6989586621679517807 infixl 7

Instances

(SNum a, SingI d) => SingI ((*@#@$$) d :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((*@#@$$) d)

SuppressUnusedWarnings ((*@#@$$) a6989586621679517806 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((*@#@$$) a6989586621679517806 :: TyFun a a -> Type) (a6989586621679517807 :: a)

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

data NegateSym0 a6989586621679517810

Instances

SNum a => SingI (NegateSym0 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing NegateSym0

SuppressUnusedWarnings (NegateSym0 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply (NegateSym0 :: TyFun a a -> Type) (a6989586621679517810 :: a)

Defined in Data.Singletons.Prelude.Num

type Apply (NegateSym0 :: TyFun a a -> Type) (a6989586621679517810 :: a) = NegateSym1 a6989586621679517810

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

data AbsSym0 a6989586621679517813

Instances

SNum a => SingI (AbsSym0 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing AbsSym0

SuppressUnusedWarnings (AbsSym0 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply (AbsSym0 :: TyFun a a -> Type) (a6989586621679517813 :: a)

Defined in Data.Singletons.Prelude.Num

type Apply (AbsSym0 :: TyFun a a -> Type) (a6989586621679517813 :: a) = AbsSym1 a6989586621679517813

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

data SignumSym0 a6989586621679517816

Instances

SNum a => SingI (SignumSym0 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing SignumSym0

SuppressUnusedWarnings (SignumSym0 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply (SignumSym0 :: TyFun a a -> Type) (a6989586621679517816 :: a)

Defined in Data.Singletons.Prelude.Num

type Apply (SignumSym0 :: TyFun a a -> Type) (a6989586621679517816 :: a) = SignumSym1 a6989586621679517816

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

data FromIntegerSym0 a6989586621679517819

Instances

SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing FromIntegerSym0

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (a6989586621679517819 :: Nat)

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

data SubtractSym0 a6989586621679517789

Instances

SNum a => SingI (SubtractSym0 :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing SubtractSym0

SuppressUnusedWarnings (SubtractSym0 :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply (SubtractSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679517789 :: a)

Defined in Data.Singletons.Prelude.Num

type Apply (SubtractSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679517789 :: a) = SubtractSym1 a6989586621679517789

data SubtractSym1 a6989586621679517789 a6989586621679517790

Instances

(SNum a, SingI d) => SingI (SubtractSym1 d :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (SubtractSym1 d)

SuppressUnusedWarnings (SubtractSym1 a6989586621679517789 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply (SubtractSym1 a6989586621679517789 :: TyFun a a -> Type) (a6989586621679517790 :: a)

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