Copyright	(C) 2014 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Promotion.Prelude.Num

Contents

Defunctionalization symbols

Description

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

Synopsis

class PNum (a :: Type) where
- type (arg :: a) + (arg :: a) :: a
- type (arg :: a) - (arg :: a) :: a
- type (arg :: a) * (arg :: a) :: a
- type Negate (arg :: a) :: a
- type Abs (arg :: a) :: a
- type Signum (arg :: a) :: a
- type FromInteger (arg :: Nat) :: a
type family Subtract (a :: a) (a :: a) :: a where ...
data (+@#@$) (l :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type))
data (l :: a6989586621679440260) +@#@$$ (l :: TyFun a6989586621679440260 a6989586621679440260)
type (+@#@$$$) (t :: a6989586621679440260) (t :: a6989586621679440260) = (+) t t
data (-@#@$) (l :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type))
data (l :: a6989586621679440260) -@#@$$ (l :: TyFun a6989586621679440260 a6989586621679440260)
type (-@#@$$$) (t :: a6989586621679440260) (t :: a6989586621679440260) = (-) t t
data (*@#@$) (l :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type))
data (l :: a6989586621679440260) *@#@$$ (l :: TyFun a6989586621679440260 a6989586621679440260)
type (*@#@$$$) (t :: a6989586621679440260) (t :: a6989586621679440260) = * t t
data NegateSym0 (l :: TyFun a6989586621679440260 a6989586621679440260)
type NegateSym1 (t :: a6989586621679440260) = Negate t
data AbsSym0 (l :: TyFun a6989586621679440260 a6989586621679440260)
type AbsSym1 (t :: a6989586621679440260) = Abs t
data SignumSym0 (l :: TyFun a6989586621679440260 a6989586621679440260)
type SignumSym1 (t :: a6989586621679440260) = Signum t
data FromIntegerSym0 (l :: TyFun Nat a6989586621679440260)
type FromIntegerSym1 (t :: Nat) = FromInteger t
data SubtractSym0 (l :: TyFun a6989586621679442533 (TyFun a6989586621679442533 a6989586621679442533 -> Type))
data SubtractSym1 (l :: a6989586621679442533) (l :: TyFun a6989586621679442533 a6989586621679442533)
type SubtractSym2 (t :: a6989586621679442533) (t :: a6989586621679442533) = Subtract t t

Documentation

class PNum (a :: Type) Source #

Associated Types

type (arg :: a) + (arg :: a) :: a Source #

type (arg :: a) - (arg :: a) :: a Source #

type (arg :: a) * (arg :: a) :: a Source #

type Negate (arg :: a) :: a Source #

type Abs (arg :: a) :: a Source #

type Signum (arg :: a) :: a Source #

type FromInteger (arg :: Nat) :: a Source #

Instances

PNum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Num Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #

type family Subtract (a :: a) (a :: a) :: a where ... Source #

Equations

Subtract x y = Apply (Apply (-@#@$) y) x

Defunctionalization symbols

data (+@#@$) (l :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type)) Source #

Instances

SuppressUnusedWarnings ((+@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((+@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> *) (l :: a6989586621679440260) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((+@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> *) (l :: a6989586621679440260) = (+@#@$$) l

data (l :: a6989586621679440260) +@#@$$ (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

SuppressUnusedWarnings ((+@#@$$) :: a6989586621679440260 -> TyFun a6989586621679440260 a6989586621679440260 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 + l2

type (+@#@$$$) (t :: a6989586621679440260) (t :: a6989586621679440260) = (+) t t Source #

data (-@#@$) (l :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type)) Source #

Instances

SuppressUnusedWarnings ((-@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((-@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> *) (l :: a6989586621679440260) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((-@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> *) (l :: a6989586621679440260) = (-@#@$$) l

data (l :: a6989586621679440260) -@#@$$ (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

SuppressUnusedWarnings ((-@#@$$) :: a6989586621679440260 -> TyFun a6989586621679440260 a6989586621679440260 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 - l2

type (-@#@$$$) (t :: a6989586621679440260) (t :: a6989586621679440260) = (-) t t Source #

data (*@#@$) (l :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type)) Source #

Instances

SuppressUnusedWarnings ((@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> ) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> ) (l :: a6989586621679440260) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> ) (l :: a6989586621679440260) = (*@#@$$) l

data (l :: a6989586621679440260) *@#@$$ (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

SuppressUnusedWarnings ((@#@$$) :: a6989586621679440260 -> TyFun a6989586621679440260 a6989586621679440260 -> ) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a) = l1 * l2

type (*@#@$$$) (t :: a6989586621679440260) (t :: a6989586621679440260) = * t t Source #

data NegateSym0 (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

SuppressUnusedWarnings (NegateSym0 :: TyFun a6989586621679440260 a6989586621679440260 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (NegateSym0 :: TyFun a a -> *) (l :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (NegateSym0 :: TyFun a a -> *) (l :: a) = Negate l

type NegateSym1 (t :: a6989586621679440260) = Negate t Source #

data AbsSym0 (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

SuppressUnusedWarnings (AbsSym0 :: TyFun a6989586621679440260 a6989586621679440260 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (AbsSym0 :: TyFun a a -> *) (l :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (AbsSym0 :: TyFun a a -> *) (l :: a) = Abs l

type AbsSym1 (t :: a6989586621679440260) = Abs t Source #

data SignumSym0 (l :: TyFun a6989586621679440260 a6989586621679440260) Source #

Instances

SuppressUnusedWarnings (SignumSym0 :: TyFun a6989586621679440260 a6989586621679440260 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (SignumSym0 :: TyFun a a -> *) (l :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SignumSym0 :: TyFun a a -> *) (l :: a) = Signum l

type SignumSym1 (t :: a6989586621679440260) = Signum t Source #

data FromIntegerSym0 (l :: TyFun Nat a6989586621679440260) Source #

Instances

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679440260 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) = (FromInteger l :: k2)

type FromIntegerSym1 (t :: Nat) = FromInteger t Source #

data SubtractSym0 (l :: TyFun a6989586621679442533 (TyFun a6989586621679442533 a6989586621679442533 -> Type)) Source #

Instances

SuppressUnusedWarnings (SubtractSym0 :: TyFun a6989586621679442533 (TyFun a6989586621679442533 a6989586621679442533 -> Type) -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (SubtractSym0 :: TyFun a6989586621679442533 (TyFun a6989586621679442533 a6989586621679442533 -> Type) -> *) (l :: a6989586621679442533) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SubtractSym0 :: TyFun a6989586621679442533 (TyFun a6989586621679442533 a6989586621679442533 -> Type) -> *) (l :: a6989586621679442533) = SubtractSym1 l

data SubtractSym1 (l :: a6989586621679442533) (l :: TyFun a6989586621679442533 a6989586621679442533) Source #

Instances

SuppressUnusedWarnings (SubtractSym1 :: a6989586621679442533 -> TyFun a6989586621679442533 a6989586621679442533 -> *) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply (SubtractSym1 l1 :: TyFun a a -> *) (l2 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply (SubtractSym1 l1 :: TyFun a a -> *) (l2 :: a) = Subtract l1 l2

type SubtractSym2 (t :: a6989586621679442533) (t :: a6989586621679442533) = Subtract t t Source #

SuppressUnusedWarnings ((@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> ) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> ) (l :: a6989586621679440260) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$) :: TyFun a6989586621679440260 (TyFun a6989586621679440260 a6989586621679440260 -> Type) -> ) (l :: a6989586621679440260) = (*@#@$$) l

SuppressUnusedWarnings ((@#@$$) :: a6989586621679440260 -> TyFun a6989586621679440260 a6989586621679440260 -> ) Source #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () Source #
type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a) = l1 * l2