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 a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type))
data (l :: a6989586621679428868) +@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868)
type (+@#@$$$) (t :: a6989586621679428868) (t :: a6989586621679428868) = (+) t t
data (-@#@$) (l :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type))
data (l :: a6989586621679428868) -@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868)
type (-@#@$$$) (t :: a6989586621679428868) (t :: a6989586621679428868) = (-) t t
data (*@#@$) (l :: TyFun a6989586621679428868 (TyFun a6989586621679428868 a6989586621679428868 -> Type))
data (l :: a6989586621679428868) *@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868)
type (*@#@$$$) (t :: a6989586621679428868) (t :: a6989586621679428868) = * t t
data NegateSym0 (l :: TyFun a6989586621679428868 a6989586621679428868)
type NegateSym1 (t :: a6989586621679428868) = Negate t
data AbsSym0 (l :: TyFun a6989586621679428868 a6989586621679428868)
type AbsSym1 (t :: a6989586621679428868) = Abs t
data SignumSym0 (l :: TyFun a6989586621679428868 a6989586621679428868)
type SignumSym1 (t :: a6989586621679428868) = Signum t
data FromIntegerSym0 (l :: TyFun Nat a6989586621679428868)
type FromIntegerSym1 (t :: Nat) = FromInteger t
data SubtractSym0 (l :: TyFun a6989586621679431141 (TyFun a6989586621679431141 a6989586621679431141 -> Type))
data SubtractSym1 (l :: a6989586621679431141) (l :: TyFun a6989586621679431141 a6989586621679431141)
type SubtractSym2 (t :: a6989586621679431141) (t :: a6989586621679431141) = Subtract t t

Documentation

class PNum (a :: Type) #

Associated Types

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 #

Instances

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

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

Equations

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

Defunctionalization symbols

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

Instances

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

data (l :: a6989586621679428868) +@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

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

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

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

Instances

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

data (l :: a6989586621679428868) -@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

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

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

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

Instances

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

data (l :: a6989586621679428868) *@#@$$ (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

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

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

data NegateSym0 (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

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

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

data AbsSym0 (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

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

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

data SignumSym0 (l :: TyFun a6989586621679428868 a6989586621679428868) #

Instances

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

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

data FromIntegerSym0 (l :: TyFun Nat a6989586621679428868) #

Instances

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679428868 -> *) #
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) #
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 #

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

Instances

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

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

Instances

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

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

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

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