Data.Singletons.Prelude.Num

Defines and exports promoted and singleton versions of definitions from GHC.Num.

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

Associated Types

type (Nat :+ (arg :: Nat)) (arg :: Nat) :: a

type (Nat :- (arg :: Nat)) (arg :: Nat) :: a

type (Nat :* (arg :: Nat)) (arg :: Nat) :: a

type Negate Nat (arg :: Nat) :: a

type Abs Nat (arg :: Nat) :: a

type Signum Nat (arg :: Nat) :: a

type FromInteger Nat (arg :: Nat) :: 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_6989586621679410569Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (:-$) t) t :: a) infixl 6

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

Instances

SNum Nat

Methods

(%:+) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:+$) Nat) t) t)

(%:-) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:-$) Nat) t) t)

(%:*) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:*$) Nat) t) t)

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

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

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

sFromInteger :: Sing Nat t -> Sing Nat (Apply Nat Nat (FromIntegerSym0 Nat) 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 a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type))

Instances

SuppressUnusedWarnings (TyFun a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type) -> *) ((:+$) a6989586621679410509)

Methods

suppressUnusedWarnings :: Proxy ((:+$) a6989586621679410509) t -> ()

type Apply a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type) ((:+$) a6989586621679410509) l

type Apply a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type) ((:+$) a6989586621679410509) l = (:+$$) a6989586621679410509 l

data (l :: a6989586621679410509) :+$$ (l :: TyFun a6989586621679410509 a6989586621679410509)

Instances

SuppressUnusedWarnings (a6989586621679410509 -> TyFun a6989586621679410509 a6989586621679410509 -> *) ((:+$$) a6989586621679410509)

Methods

suppressUnusedWarnings :: Proxy ((:+$$) a6989586621679410509) t -> ()

type Apply a a ((:+$$) a l1) l2

type Apply a a ((:+$$) a l1) l2 = (:+) a l1 l2

type (:+$$$) (t :: a6989586621679410509) (t :: a6989586621679410509) = (:+) t t

data (:-$) (l :: TyFun a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type))

Instances

SuppressUnusedWarnings (TyFun a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type) -> *) ((:-$) a6989586621679410509)

Methods

suppressUnusedWarnings :: Proxy ((:-$) a6989586621679410509) t -> ()

type Apply a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type) ((:-$) a6989586621679410509) l

type Apply a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type) ((:-$) a6989586621679410509) l = (:-$$) a6989586621679410509 l

data (l :: a6989586621679410509) :-$$ (l :: TyFun a6989586621679410509 a6989586621679410509)

Instances

SuppressUnusedWarnings (a6989586621679410509 -> TyFun a6989586621679410509 a6989586621679410509 -> *) ((:-$$) a6989586621679410509)

Methods

suppressUnusedWarnings :: Proxy ((:-$$) a6989586621679410509) t -> ()

type Apply a a ((:-$$) a l1) l2

type Apply a a ((:-$$) a l1) l2 = (:-) a l1 l2

type (:-$$$) (t :: a6989586621679410509) (t :: a6989586621679410509) = (:-) t t

data (:*$) (l :: TyFun a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type))

Instances

SuppressUnusedWarnings (TyFun a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type) -> *) ((:*$) a6989586621679410509)

Methods

suppressUnusedWarnings :: Proxy ((:*$) a6989586621679410509) t -> ()

type Apply a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type) ((:*$) a6989586621679410509) l

type Apply a6989586621679410509 (TyFun a6989586621679410509 a6989586621679410509 -> Type) ((:*$) a6989586621679410509) l = (:*$$) a6989586621679410509 l

data (l :: a6989586621679410509) :*$$ (l :: TyFun a6989586621679410509 a6989586621679410509)

Instances

SuppressUnusedWarnings (a6989586621679410509 -> TyFun a6989586621679410509 a6989586621679410509 -> *) ((:*$$) a6989586621679410509)

Methods

suppressUnusedWarnings :: Proxy ((:*$$) a6989586621679410509) t -> ()

type Apply a a ((:*$$) a l1) l2

type Apply a a ((:*$$) a l1) l2 = (:*) a l1 l2

type (:*$$$) (t :: a6989586621679410509) (t :: a6989586621679410509) = (:*) t t

data NegateSym0 (l :: TyFun a6989586621679410509 a6989586621679410509)

Instances

SuppressUnusedWarnings (TyFun a6989586621679410509 a6989586621679410509 -> *) (NegateSym0 a6989586621679410509)

Methods

suppressUnusedWarnings :: Proxy (NegateSym0 a6989586621679410509) t -> ()

type Apply a a (NegateSym0 a) l

type Apply a a (NegateSym0 a) l = Negate a l

type NegateSym1 (t :: a6989586621679410509) = Negate t

data AbsSym0 (l :: TyFun a6989586621679410509 a6989586621679410509)

Instances

SuppressUnusedWarnings (TyFun a6989586621679410509 a6989586621679410509 -> *) (AbsSym0 a6989586621679410509)

Methods

suppressUnusedWarnings :: Proxy (AbsSym0 a6989586621679410509) t -> ()

type Apply a a (AbsSym0 a) l

type Apply a a (AbsSym0 a) l = Abs a l

type AbsSym1 (t :: a6989586621679410509) = Abs t

data SignumSym0 (l :: TyFun a6989586621679410509 a6989586621679410509)

Instances

SuppressUnusedWarnings (TyFun a6989586621679410509 a6989586621679410509 -> *) (SignumSym0 a6989586621679410509)

Methods

suppressUnusedWarnings :: Proxy (SignumSym0 a6989586621679410509) t -> ()

type Apply a a (SignumSym0 a) l

type Apply a a (SignumSym0 a) l = Signum a l

type SignumSym1 (t :: a6989586621679410509) = Signum t

data FromIntegerSym0 (l :: TyFun Nat a6989586621679410509)

Instances

SuppressUnusedWarnings (TyFun Nat a6989586621679410509 -> *) (FromIntegerSym0 a6989586621679410509)

Methods

suppressUnusedWarnings :: Proxy (FromIntegerSym0 a6989586621679410509) t -> ()

type Apply Nat k2 (FromIntegerSym0 k2) l

type Apply Nat k2 (FromIntegerSym0 k2) l = FromInteger k2 l

type FromIntegerSym1 (t :: Nat) = FromInteger t

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

Instances

SuppressUnusedWarnings (TyFun a6989586621679412800 (TyFun a6989586621679412800 a6989586621679412800 -> Type) -> *) (SubtractSym0 a6989586621679412800)

Methods

suppressUnusedWarnings :: Proxy (SubtractSym0 a6989586621679412800) t -> ()

type Apply a6989586621679412800 (TyFun a6989586621679412800 a6989586621679412800 -> Type) (SubtractSym0 a6989586621679412800) l

type Apply a6989586621679412800 (TyFun a6989586621679412800 a6989586621679412800 -> Type) (SubtractSym0 a6989586621679412800) l = SubtractSym1 a6989586621679412800 l

data SubtractSym1 (l :: a6989586621679412800) (l :: TyFun a6989586621679412800 a6989586621679412800)

Instances

SuppressUnusedWarnings (a6989586621679412800 -> TyFun a6989586621679412800 a6989586621679412800 -> *) (SubtractSym1 a6989586621679412800)

Methods

suppressUnusedWarnings :: Proxy (SubtractSym1 a6989586621679412800) t -> ()

type Apply a a (SubtractSym1 a l1) l2

type Apply a a (SubtractSym1 a l1) l2 = Subtract a l1 l2

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