singletons-2.3.1: A framework for generating singleton types

Copyright(C) 2014 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (rae@cs.brynmawr.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Prelude.Num

Contents

Description

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

Synopsis

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

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

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 a6989586621679348813 (TyFun a6989586621679348813 a6989586621679348813 -> Type)) #

Instances

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

Methods

suppressUnusedWarnings :: Proxy ((:+$) a6989586621679348813) t -> () #

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

data (l :: a6989586621679348813) :+$$ (l :: TyFun a6989586621679348813 a6989586621679348813) #

Instances

SuppressUnusedWarnings (a6989586621679348813 -> TyFun a6989586621679348813 a6989586621679348813 -> *) ((:+$$) a6989586621679348813) # 

Methods

suppressUnusedWarnings :: Proxy ((:+$$) a6989586621679348813) t -> () #

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

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

data (:-$) (l :: TyFun a6989586621679348813 (TyFun a6989586621679348813 a6989586621679348813 -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a6989586621679348813 (TyFun a6989586621679348813 a6989586621679348813 -> Type) -> *) ((:-$) a6989586621679348813) # 

Methods

suppressUnusedWarnings :: Proxy ((:-$) a6989586621679348813) t -> () #

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

data (l :: a6989586621679348813) :-$$ (l :: TyFun a6989586621679348813 a6989586621679348813) #

Instances

SuppressUnusedWarnings (a6989586621679348813 -> TyFun a6989586621679348813 a6989586621679348813 -> *) ((:-$$) a6989586621679348813) # 

Methods

suppressUnusedWarnings :: Proxy ((:-$$) a6989586621679348813) t -> () #

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

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

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

Instances

SuppressUnusedWarnings (TyFun a6989586621679348813 (TyFun a6989586621679348813 a6989586621679348813 -> Type) -> *) ((:*$) a6989586621679348813) # 

Methods

suppressUnusedWarnings :: Proxy ((:*$) a6989586621679348813) t -> () #

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

data (l :: a6989586621679348813) :*$$ (l :: TyFun a6989586621679348813 a6989586621679348813) #

Instances

SuppressUnusedWarnings (a6989586621679348813 -> TyFun a6989586621679348813 a6989586621679348813 -> *) ((:*$$) a6989586621679348813) # 

Methods

suppressUnusedWarnings :: Proxy ((:*$$) a6989586621679348813) t -> () #

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

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

data NegateSym0 (l :: TyFun a6989586621679348813 a6989586621679348813) #

Instances

SuppressUnusedWarnings (TyFun a6989586621679348813 a6989586621679348813 -> *) (NegateSym0 a6989586621679348813) # 

Methods

suppressUnusedWarnings :: Proxy (NegateSym0 a6989586621679348813) t -> () #

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

type NegateSym1 (t :: a6989586621679348813) = Negate t #

data AbsSym0 (l :: TyFun a6989586621679348813 a6989586621679348813) #

Instances

SuppressUnusedWarnings (TyFun a6989586621679348813 a6989586621679348813 -> *) (AbsSym0 a6989586621679348813) # 

Methods

suppressUnusedWarnings :: Proxy (AbsSym0 a6989586621679348813) t -> () #

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

type AbsSym1 (t :: a6989586621679348813) = Abs t #

data SignumSym0 (l :: TyFun a6989586621679348813 a6989586621679348813) #

Instances

SuppressUnusedWarnings (TyFun a6989586621679348813 a6989586621679348813 -> *) (SignumSym0 a6989586621679348813) # 

Methods

suppressUnusedWarnings :: Proxy (SignumSym0 a6989586621679348813) t -> () #

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

type SignumSym1 (t :: a6989586621679348813) = Signum t #

data FromIntegerSym0 (l :: TyFun Nat a6989586621679348813) #

Instances

SuppressUnusedWarnings (TyFun Nat a6989586621679348813 -> *) (FromIntegerSym0 a6989586621679348813) # 

Methods

suppressUnusedWarnings :: Proxy (FromIntegerSym0 a6989586621679348813) t -> () #

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

data SubtractSym0 (l :: TyFun a6989586621679351104 (TyFun a6989586621679351104 a6989586621679351104 -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a6989586621679351104 (TyFun a6989586621679351104 a6989586621679351104 -> Type) -> *) (SubtractSym0 a6989586621679351104) # 

Methods

suppressUnusedWarnings :: Proxy (SubtractSym0 a6989586621679351104) t -> () #

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

data SubtractSym1 (l :: a6989586621679351104) (l :: TyFun a6989586621679351104 a6989586621679351104) #

Instances

SuppressUnusedWarnings (a6989586621679351104 -> TyFun a6989586621679351104 a6989586621679351104 -> *) (SubtractSym1 a6989586621679351104) # 

Methods

suppressUnusedWarnings :: Proxy (SubtractSym1 a6989586621679351104) t -> () #

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

type SubtractSym2 (t :: a6989586621679351104) (t :: a6989586621679351104) = Subtract t t #