Copyright	(C) 2014 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (eir@cis.upenn.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 (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

PNum Nat (KProxy Nat) Source

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

SNum Nat (KProxy Nat) Source

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

SuppressUnusedWarnings (TyFun k k -> *) (NegateSym0 k) Source
type Apply k k (NegateSym0 k) l0 = NegateSym1 k l0 Source

type NegateSym1 t = Negate t Source

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

SuppressUnusedWarnings (TyFun k k -> *) (SignumSym0 k) Source
type Apply k k (SignumSym0 k) l0 = SignumSym1 k l0 Source

type SignumSym1 t = Signum t Source

data FromIntegerSym0 l Source

Instances

SuppressUnusedWarnings (TyFun Nat k -> *) (FromIntegerSym0 k) Source
type Apply k Nat (FromIntegerSym0 k) l0 = FromIntegerSym1 k l0 Source

type FromIntegerSym1 t = FromInteger t Source

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

type SubtractSym2 t t = Subtract t t Source