singletons-2.0.1: 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 ~ KProxy) => PNum kproxy Source

Associated Types

type arg :+ arg :: a infixl 6 Source

type arg :- arg :: a infixl 6 Source

type arg :* arg :: a infixl 7 Source

type Negate arg :: a Source

type Abs arg :: a Source

type Signum arg :: a Source

type FromInteger arg :: a Source

Instances

class (kproxy ~ KProxy) => SNum kproxy where Source

Minimal complete definition

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

Methods

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

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

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

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

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

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

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

Instances

type family Subtract a a :: a Source

Equations

Subtract x y = Apply (Apply (:-$) y) x 

sSubtract :: forall t t. SNum (KProxy :: KProxy a) => Sing t -> Sing t -> Sing (Apply (Apply SubtractSym0 t) t :: a) Source

Defunctionalization symbols

data (:+$) l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) ((:+$) k) Source 
type Apply (TyFun k k -> *) k ((:+$) k) l0 = (:+$$) k l0 Source 

data l :+$$ l Source

Instances

SuppressUnusedWarnings (k -> TyFun k k -> *) ((:+$$) k) Source 
type Apply k k ((:+$$) k l1) l0 = (:+$$$) k l1 l0 Source 

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

data (:-$) l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) ((:-$) k) Source 
type Apply (TyFun k k -> *) k ((:-$) k) l0 = (:-$$) k l0 Source 

data l :-$$ l Source

Instances

SuppressUnusedWarnings (k -> TyFun k k -> *) ((:-$$) k) Source 
type Apply k k ((:-$$) k l1) l0 = (:-$$$) k l1 l0 Source 

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

data (:*$) l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) ((:*$) k) Source 
type Apply (TyFun k k -> *) k ((:*$) k) l0 = (:*$$) k l0 Source 

data l :*$$ l Source

Instances

SuppressUnusedWarnings (k -> TyFun k k -> *) ((:*$$) k) Source 
type Apply k k ((:*$$) k l1) l0 = (:*$$$) k l1 l0 Source 

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

data NegateSym0 l Source

Instances

data AbsSym0 l Source

Instances

SuppressUnusedWarnings (TyFun k k -> *) (AbsSym0 k) Source 
type Apply k k (AbsSym0 k) l0 = AbsSym1 k l0 Source 

type AbsSym1 t = Abs t Source

data SignumSym0 l Source

Instances

data SubtractSym0 l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) (SubtractSym0 k) Source 
type Apply (TyFun k k -> *) k (SubtractSym0 k) l0 = SubtractSym1 k l0 Source 

data SubtractSym1 l l Source

Instances

SuppressUnusedWarnings (k -> TyFun k k -> *) (SubtractSym1 k) Source 
type Apply k k (SubtractSym1 k l1) l0 = SubtractSym2 k l1 l0 Source