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.Singletons.Prelude.Num

Contents

Defunctionalization symbols

Description

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

Synopsis

Documentation

class PNum (a :: Type) #

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 #
Associated Types type (Nat :+ (arg :: Nat)) (arg :: Nat) :: a # type (Nat :- (arg :: Nat)) (arg :: Nat) :: a # type (Nat :* (arg :: Nat)) (arg :: Nat) :: a # type Negate Nat (arg :: Nat) :: a # type Abs Nat (arg :: Nat) :: a # type Signum Nat (arg :: Nat) :: a # type FromInteger Nat (arg :: Nat) :: a #

class SNum a where #

Minimal complete definition

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

Methods

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

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

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

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

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

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

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

(%:-) :: forall (t :: a) (t :: a). ((Apply (Apply (:-$) t) t :: a) ~ Apply (Apply TFHelper_1627807434Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (:-$) t) t :: a) infixl 6 #

sNegate :: forall (t :: a). ((Apply NegateSym0 t :: a) ~ Apply Negate_1627807449Sym0 t) => Sing t -> Sing (Apply NegateSym0 t :: a) #

Instances

SNum Nat #

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

Equations

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

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

Defunctionalization symbols

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

Instances

SuppressUnusedWarnings (TyFun a1627807374 (TyFun a1627807374 a1627807374 -> Type) -> *) ((:+$) a1627807374) #
Methods suppressUnusedWarnings :: Proxy ((:+$) a1627807374) t -> () #
type Apply a1627807374 (TyFun a1627807374 a1627807374 -> Type) ((:+$) a1627807374) l #
type Apply a1627807374 (TyFun a1627807374 a1627807374 -> Type) ((:+$) a1627807374) l = (:+$$) a1627807374 l

data (l :: a1627807374) :+$$ (l :: TyFun a1627807374 a1627807374) #

Instances

SuppressUnusedWarnings (a1627807374 -> TyFun a1627807374 a1627807374 -> *) ((:+$$) a1627807374) #
Methods suppressUnusedWarnings :: Proxy ((:+$$) a1627807374) t -> () #
type Apply a a ((:+$$) a l1) l2 #
type Apply a a ((:+$$) a l1) l2 = (:+) a l1 l2

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

data (:-$) (l :: TyFun a1627807374 (TyFun a1627807374 a1627807374 -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a1627807374 (TyFun a1627807374 a1627807374 -> Type) -> *) ((:-$) a1627807374) #
Methods suppressUnusedWarnings :: Proxy ((:-$) a1627807374) t -> () #
type Apply a1627807374 (TyFun a1627807374 a1627807374 -> Type) ((:-$) a1627807374) l #
type Apply a1627807374 (TyFun a1627807374 a1627807374 -> Type) ((:-$) a1627807374) l = (:-$$) a1627807374 l

data (l :: a1627807374) :-$$ (l :: TyFun a1627807374 a1627807374) #

Instances

SuppressUnusedWarnings (a1627807374 -> TyFun a1627807374 a1627807374 -> *) ((:-$$) a1627807374) #
Methods suppressUnusedWarnings :: Proxy ((:-$$) a1627807374) t -> () #
type Apply a a ((:-$$) a l1) l2 #
type Apply a a ((:-$$) a l1) l2 = (:-) a l1 l2

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

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

Instances

SuppressUnusedWarnings (TyFun a1627807374 (TyFun a1627807374 a1627807374 -> Type) -> ) ((:$) a1627807374) #
Methods suppressUnusedWarnings :: Proxy ((:*$) a1627807374) t -> () #
type Apply a1627807374 (TyFun a1627807374 a1627807374 -> Type) ((:*$) a1627807374) l #
type Apply a1627807374 (TyFun a1627807374 a1627807374 -> Type) ((:$) a1627807374) l = (:$$) a1627807374 l

data (l :: a1627807374) :*$$ (l :: TyFun a1627807374 a1627807374) #

Instances

SuppressUnusedWarnings (a1627807374 -> TyFun a1627807374 a1627807374 -> ) ((:$$) a1627807374) #
Methods suppressUnusedWarnings :: Proxy ((:*$$) a1627807374) t -> () #
type Apply a a ((:*$$) a l1) l2 #
type Apply a a ((:$$) a l1) l2 = (:) a l1 l2

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

data NegateSym0 (l :: TyFun a1627807374 a1627807374) #

Instances

SuppressUnusedWarnings (TyFun a1627807374 a1627807374 -> *) (NegateSym0 a1627807374) #
Methods suppressUnusedWarnings :: Proxy (NegateSym0 a1627807374) t -> () #
type Apply a a (NegateSym0 a) l #
type Apply a a (NegateSym0 a) l = Negate a l

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

data AbsSym0 (l :: TyFun a1627807374 a1627807374) #

Instances

SuppressUnusedWarnings (TyFun a1627807374 a1627807374 -> *) (AbsSym0 a1627807374) #
Methods suppressUnusedWarnings :: Proxy (AbsSym0 a1627807374) t -> () #
type Apply a a (AbsSym0 a) l #
type Apply a a (AbsSym0 a) l = Abs a l

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

data SignumSym0 (l :: TyFun a1627807374 a1627807374) #

Instances

SuppressUnusedWarnings (TyFun a1627807374 a1627807374 -> *) (SignumSym0 a1627807374) #
Methods suppressUnusedWarnings :: Proxy (SignumSym0 a1627807374) t -> () #
type Apply a a (SignumSym0 a) l #
type Apply a a (SignumSym0 a) l = Signum a l

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

data FromIntegerSym0 (l :: TyFun Nat a1627807374) #

Instances

SuppressUnusedWarnings (TyFun Nat a1627807374 -> *) (FromIntegerSym0 a1627807374) #
Methods suppressUnusedWarnings :: Proxy (FromIntegerSym0 a1627807374) t -> () #
type Apply Nat k2 (FromIntegerSym0 k2) l #
type Apply Nat k2 (FromIntegerSym0 k2) l = FromInteger k2 l

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

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

Instances

SuppressUnusedWarnings (TyFun a1627809665 (TyFun a1627809665 a1627809665 -> Type) -> *) (SubtractSym0 a1627809665) #
Methods suppressUnusedWarnings :: Proxy (SubtractSym0 a1627809665) t -> () #
type Apply a1627809665 (TyFun a1627809665 a1627809665 -> Type) (SubtractSym0 a1627809665) l #
type Apply a1627809665 (TyFun a1627809665 a1627809665 -> Type) (SubtractSym0 a1627809665) l = SubtractSym1 a1627809665 l

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

Instances

SuppressUnusedWarnings (a1627809665 -> TyFun a1627809665 a1627809665 -> *) (SubtractSym1 a1627809665) #
Methods suppressUnusedWarnings :: Proxy (SubtractSym1 a1627809665) t -> () #
type Apply a a (SubtractSym1 a l1) l2 #
type Apply a a (SubtractSym1 a l1) l2 = Subtract a l1 l2

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