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 :: Type)

Associated Types

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

Instances

PNum Nat

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_6989586621679412590Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t :: a) infixl 6

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

Instances

SNum Nat

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 (t :: a) (t :: a). SNum a => Sing t -> Sing t -> Sing (Apply (Apply SubtractSym0 t) t :: a)

Defunctionalization symbols

data (+@#@$) (l :: TyFun a6989586621679412530 (TyFun a6989586621679412530 a6989586621679412530 -> Type))

Instances

SuppressUnusedWarnings ((+@#@$) :: TyFun a6989586621679412530 (TyFun a6989586621679412530 a6989586621679412530 -> Type) -> *)

Methods

suppressUnusedWarnings :: ()

type Apply ((+@#@$) :: TyFun a6989586621679412530 (TyFun a6989586621679412530 a6989586621679412530 -> Type) -> *) (l :: a6989586621679412530)

type Apply ((+@#@$) :: TyFun a6989586621679412530 (TyFun a6989586621679412530 a6989586621679412530 -> Type) -> *) (l :: a6989586621679412530) = (+@#@$$) l

data (l :: a6989586621679412530) +@#@$$ (l :: TyFun a6989586621679412530 a6989586621679412530)

Instances

SuppressUnusedWarnings ((+@#@$$) :: a6989586621679412530 -> TyFun a6989586621679412530 a6989586621679412530 -> *)

Methods

suppressUnusedWarnings :: ()

type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a)

type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 + l2

type (+@#@$$$) (t :: a6989586621679412530) (t :: a6989586621679412530) = (+) t t

data (-@#@$) (l :: TyFun a6989586621679412530 (TyFun a6989586621679412530 a6989586621679412530 -> Type))

Instances

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

Methods

suppressUnusedWarnings :: ()

type Apply ((-@#@$) :: TyFun a6989586621679412530 (TyFun a6989586621679412530 a6989586621679412530 -> Type) -> *) (l :: a6989586621679412530)

type Apply ((-@#@$) :: TyFun a6989586621679412530 (TyFun a6989586621679412530 a6989586621679412530 -> Type) -> *) (l :: a6989586621679412530) = (-@#@$$) l

data (l :: a6989586621679412530) -@#@$$ (l :: TyFun a6989586621679412530 a6989586621679412530)

Instances

SuppressUnusedWarnings ((-@#@$$) :: a6989586621679412530 -> TyFun a6989586621679412530 a6989586621679412530 -> *)

Methods

suppressUnusedWarnings :: ()

type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a)

type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 - l2

type (-@#@$$$) (t :: a6989586621679412530) (t :: a6989586621679412530) = (-) t t

data (*@#@$) (l :: TyFun a6989586621679412530 (TyFun a6989586621679412530 a6989586621679412530 -> Type))

Instances

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

Methods

suppressUnusedWarnings :: ()

type Apply ((*@#@$) :: TyFun a6989586621679412530 (TyFun a6989586621679412530 a6989586621679412530 -> Type) -> *) (l :: a6989586621679412530)

type Apply ((*@#@$) :: TyFun a6989586621679412530 (TyFun a6989586621679412530 a6989586621679412530 -> Type) -> *) (l :: a6989586621679412530) = (*@#@$$) l

data (l :: a6989586621679412530) *@#@$$ (l :: TyFun a6989586621679412530 a6989586621679412530)

Instances

SuppressUnusedWarnings ((*@#@$$) :: a6989586621679412530 -> TyFun a6989586621679412530 a6989586621679412530 -> *)

Methods

suppressUnusedWarnings :: ()

type Apply ((*@#@$$) l1 :: TyFun a a -> *) (l2 :: a)

type Apply ((*@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 * l2

type (*@#@$$$) (t :: a6989586621679412530) (t :: a6989586621679412530) = * t t

data NegateSym0 (l :: TyFun a6989586621679412530 a6989586621679412530)

Instances

SuppressUnusedWarnings (NegateSym0 :: TyFun a6989586621679412530 a6989586621679412530 -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (NegateSym0 :: TyFun a a -> *) (l :: a)

type Apply (NegateSym0 :: TyFun a a -> *) (l :: a) = Negate l

type NegateSym1 (t :: a6989586621679412530) = Negate t

data AbsSym0 (l :: TyFun a6989586621679412530 a6989586621679412530)

Instances

SuppressUnusedWarnings (AbsSym0 :: TyFun a6989586621679412530 a6989586621679412530 -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (AbsSym0 :: TyFun a a -> *) (l :: a)

type Apply (AbsSym0 :: TyFun a a -> *) (l :: a) = Abs l

type AbsSym1 (t :: a6989586621679412530) = Abs t

data SignumSym0 (l :: TyFun a6989586621679412530 a6989586621679412530)

Instances

SuppressUnusedWarnings (SignumSym0 :: TyFun a6989586621679412530 a6989586621679412530 -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (SignumSym0 :: TyFun a a -> *) (l :: a)

type Apply (SignumSym0 :: TyFun a a -> *) (l :: a) = Signum l

type SignumSym1 (t :: a6989586621679412530) = Signum t

data FromIntegerSym0 (l :: TyFun Nat a6989586621679412530)

Instances

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679412530 -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat)

type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) = (FromInteger l :: k2)

type FromIntegerSym1 (t :: Nat) = FromInteger t

data SubtractSym0 (l :: TyFun a6989586621679414803 (TyFun a6989586621679414803 a6989586621679414803 -> Type))

Instances

SuppressUnusedWarnings (SubtractSym0 :: TyFun a6989586621679414803 (TyFun a6989586621679414803 a6989586621679414803 -> Type) -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (SubtractSym0 :: TyFun a6989586621679414803 (TyFun a6989586621679414803 a6989586621679414803 -> Type) -> *) (l :: a6989586621679414803)

type Apply (SubtractSym0 :: TyFun a6989586621679414803 (TyFun a6989586621679414803 a6989586621679414803 -> Type) -> *) (l :: a6989586621679414803) = SubtractSym1 l

data SubtractSym1 (l :: a6989586621679414803) (l :: TyFun a6989586621679414803 a6989586621679414803)

Instances

SuppressUnusedWarnings (SubtractSym1 :: a6989586621679414803 -> TyFun a6989586621679414803 a6989586621679414803 -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (SubtractSym1 l1 :: TyFun a a -> *) (l2 :: a)

type Apply (SubtractSym1 l1 :: TyFun a a -> *) (l2 :: a) = Subtract l1 l2

type SubtractSym2 (t :: a6989586621679414803) (t :: a6989586621679414803) = Subtract t t