singletons-2.4.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.Promotion.Prelude.Num

Contents

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 #