Data.Singletons.Prelude.Num

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

Documentation

class (kproxy ~ Proxy) => PNum kproxy

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 (Proxy * Nat)

Associated Types

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

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

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

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

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

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

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

class SNum a where

Minimal complete definition

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

Methods

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

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

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

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

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

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

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

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

sNegate :: forall t. (Apply NegateSym0 t ~ Apply Negate_1627817295Sym0 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 t. SNum a => Sing t -> Sing t -> Sing (Apply (Apply SubtractSym0 t) t :: a)

Defunctionalization symbols

data (:+$) l

Instances

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

Methods

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

type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:+$) a1627817219) l0

type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:+$) a1627817219) l0 = (:+$$) a1627817219 l0

data l :+$$ l

Instances

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

Methods

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

type Apply a1627817219 a1627817219 ((:+$$) a1627817219 l1) l0

type Apply a1627817219 a1627817219 ((:+$$) a1627817219 l1) l0 = (:+$$$) a1627817219 l1 l0

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

data (:-$) l

Instances

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

Methods

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

type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:-$) a1627817219) l0

type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:-$) a1627817219) l0 = (:-$$) a1627817219 l0

data l :-$$ l

Instances

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

Methods

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

type Apply a1627817219 a1627817219 ((:-$$) a1627817219 l1) l0

type Apply a1627817219 a1627817219 ((:-$$) a1627817219 l1) l0 = (:-$$$) a1627817219 l1 l0

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

data (:*$) l

Instances

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

Methods

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

type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:*$) a1627817219) l0

type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:*$) a1627817219) l0 = (:*$$) a1627817219 l0

data l :*$$ l

Instances

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

Methods

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

type Apply a1627817219 a1627817219 ((:*$$) a1627817219 l1) l0

type Apply a1627817219 a1627817219 ((:*$$) a1627817219 l1) l0 = (:*$$$) a1627817219 l1 l0

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

data NegateSym0 l

Instances

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

Methods

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

type Apply a1627817219 a1627817219 (NegateSym0 a1627817219) l0

type Apply a1627817219 a1627817219 (NegateSym0 a1627817219) l0 = NegateSym1 a1627817219 l0

type NegateSym1 t = Negate t

data AbsSym0 l

Instances

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

Methods

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

type Apply a1627817219 a1627817219 (AbsSym0 a1627817219) l0

type Apply a1627817219 a1627817219 (AbsSym0 a1627817219) l0 = AbsSym1 a1627817219 l0

type AbsSym1 t = Abs t

data SignumSym0 l

Instances

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

Methods

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

type Apply a1627817219 a1627817219 (SignumSym0 a1627817219) l0

type Apply a1627817219 a1627817219 (SignumSym0 a1627817219) l0 = SignumSym1 a1627817219 l0

type SignumSym1 t = Signum t

data FromIntegerSym0 l

Instances

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

Methods

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

type Apply Nat k2 (FromIntegerSym0 k2) l0

type Apply Nat k2 (FromIntegerSym0 k2) l0 = FromIntegerSym1 k2 l0

type FromIntegerSym1 t = FromInteger t

data SubtractSym0 l

Instances

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

Methods

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

type Apply a1627819601 (TyFun a1627819601 a1627819601 -> Type) (SubtractSym0 a1627819601) l0

type Apply a1627819601 (TyFun a1627819601 a1627819601 -> Type) (SubtractSym0 a1627819601) l0 = SubtractSym1 a1627819601 l0

data SubtractSym1 l l

Instances

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

Methods

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

type Apply a1627819601 a1627819601 (SubtractSym1 a1627819601 l1) l0

type Apply a1627819601 a1627819601 (SubtractSym1 a1627819601 l1) l0 = SubtractSym2 a1627819601 l1 l0

type SubtractSym2 t t = Subtract t t