singletons-2.2: A framework for generating singleton types

Copyright(C) 2014 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.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 (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_6989586621679685297Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (:-$) t) t :: a) infixl 6 #

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

Defunctionalization symbols

data (:+$) l #

Instances

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

Methods

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

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

data l :+$$ l #

Instances

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

Methods

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

type Apply a6989586621679685236 a6989586621679685236 ((:+$$) a6989586621679685236 l0) l1 # 
type Apply a6989586621679685236 a6989586621679685236 ((:+$$) a6989586621679685236 l0) l1 = (:+$$$) a6989586621679685236 l0 l1

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

data (:-$) l #

Instances

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

Methods

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

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

data l :-$$ l #

Instances

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

Methods

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

type Apply a6989586621679685236 a6989586621679685236 ((:-$$) a6989586621679685236 l0) l1 # 
type Apply a6989586621679685236 a6989586621679685236 ((:-$$) a6989586621679685236 l0) l1 = (:-$$$) a6989586621679685236 l0 l1

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

data (:*$) l #

Instances

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

Methods

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

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

data l :*$$ l #

Instances

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

Methods

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

type Apply a6989586621679685236 a6989586621679685236 ((:*$$) a6989586621679685236 l0) l1 # 
type Apply a6989586621679685236 a6989586621679685236 ((:*$$) a6989586621679685236 l0) l1 = (:*$$$) a6989586621679685236 l0 l1

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

data NegateSym0 l #

Instances

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

Methods

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

type Apply a6989586621679685236 a6989586621679685236 (NegateSym0 a6989586621679685236) l0 # 
type Apply a6989586621679685236 a6989586621679685236 (NegateSym0 a6989586621679685236) l0 = NegateSym1 a6989586621679685236 l0

type NegateSym1 t = Negate t #

data AbsSym0 l #

Instances

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

Methods

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

type Apply a6989586621679685236 a6989586621679685236 (AbsSym0 a6989586621679685236) l0 # 
type Apply a6989586621679685236 a6989586621679685236 (AbsSym0 a6989586621679685236) l0 = AbsSym1 a6989586621679685236 l0

type AbsSym1 t = Abs t #

data SignumSym0 l #

Instances

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

Methods

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

type Apply a6989586621679685236 a6989586621679685236 (SignumSym0 a6989586621679685236) l0 # 
type Apply a6989586621679685236 a6989586621679685236 (SignumSym0 a6989586621679685236) l0 = SignumSym1 a6989586621679685236 l0

type SignumSym1 t = Signum t #

data FromIntegerSym0 l #

Instances

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

Methods

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

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

data SubtractSym0 l #

Instances

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

Methods

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

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

data SubtractSym1 l l #

Instances

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

Methods

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

type Apply a6989586621679687552 a6989586621679687552 (SubtractSym1 a6989586621679687552 l0) l1 # 
type Apply a6989586621679687552 a6989586621679687552 (SubtractSym1 a6989586621679687552 l0) l1 = SubtractSym2 a6989586621679687552 l0 l1

type SubtractSym2 t t = Subtract t t #