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 ~ Proxy) => PNum kproxy Source #

Associated Types

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

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

type (arg :: a) :* (arg :: a) :: a infixl 7 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 (Proxy * Nat) Source #

class SNum a 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 #

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

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

Instances

SNum Nat Source #

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

Equations

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

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

Defunctionalization symbols

data (:+$) l Source #

Instances

SuppressUnusedWarnings (TyFun a1627817219 (TyFun a1627817219 a1627817219 -> Type) -> *) ((:+$) a1627817219) Source #
Methods suppressUnusedWarnings :: Proxy ((:+$) a1627817219) t -> () Source #
type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:+$) a1627817219) l0 Source #
type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:+$) a1627817219) l0 = (:+$$) a1627817219 l0

data l :+$$ l Source #

Instances

SuppressUnusedWarnings (a1627817219 -> TyFun a1627817219 a1627817219 -> *) ((:+$$) a1627817219) Source #
Methods suppressUnusedWarnings :: Proxy ((:+$$) a1627817219) t -> () Source #
type Apply a1627817219 a1627817219 ((:+$$) a1627817219 l1) l0 Source #
type Apply a1627817219 a1627817219 ((:+$$) a1627817219 l1) l0 = (:+$$$) a1627817219 l1 l0

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

data (:-$) l Source #

Instances

SuppressUnusedWarnings (TyFun a1627817219 (TyFun a1627817219 a1627817219 -> Type) -> *) ((:-$) a1627817219) Source #
Methods suppressUnusedWarnings :: Proxy ((:-$) a1627817219) t -> () Source #
type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:-$) a1627817219) l0 Source #
type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:-$) a1627817219) l0 = (:-$$) a1627817219 l0

data l :-$$ l Source #

Instances

SuppressUnusedWarnings (a1627817219 -> TyFun a1627817219 a1627817219 -> *) ((:-$$) a1627817219) Source #
Methods suppressUnusedWarnings :: Proxy ((:-$$) a1627817219) t -> () Source #
type Apply a1627817219 a1627817219 ((:-$$) a1627817219 l1) l0 Source #
type Apply a1627817219 a1627817219 ((:-$$) a1627817219 l1) l0 = (:-$$$) a1627817219 l1 l0

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

data (:*$) l Source #

Instances

SuppressUnusedWarnings (TyFun a1627817219 (TyFun a1627817219 a1627817219 -> Type) -> ) ((:$) a1627817219) Source #
Methods suppressUnusedWarnings :: Proxy ((:*$) a1627817219) t -> () Source #
type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:*$) a1627817219) l0 Source #
type Apply a1627817219 (TyFun a1627817219 a1627817219 -> Type) ((:$) a1627817219) l0 = (:$$) a1627817219 l0

data l :*$$ l Source #

Instances

SuppressUnusedWarnings (a1627817219 -> TyFun a1627817219 a1627817219 -> ) ((:$$) a1627817219) Source #
Methods suppressUnusedWarnings :: Proxy ((:*$$) a1627817219) t -> () Source #
type Apply a1627817219 a1627817219 ((:*$$) a1627817219 l1) l0 Source #
type Apply a1627817219 a1627817219 ((:$$) a1627817219 l1) l0 = (:$$$) a1627817219 l1 l0

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

data NegateSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun a1627817219 a1627817219 -> *) (NegateSym0 a1627817219) Source #
Methods suppressUnusedWarnings :: Proxy (NegateSym0 a1627817219) t -> () Source #
type Apply a1627817219 a1627817219 (NegateSym0 a1627817219) l0 Source #
type Apply a1627817219 a1627817219 (NegateSym0 a1627817219) l0 = NegateSym1 a1627817219 l0

type NegateSym1 t = Negate t Source #

data AbsSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun a1627817219 a1627817219 -> *) (AbsSym0 a1627817219) Source #
Methods suppressUnusedWarnings :: Proxy (AbsSym0 a1627817219) t -> () Source #
type Apply a1627817219 a1627817219 (AbsSym0 a1627817219) l0 Source #
type Apply a1627817219 a1627817219 (AbsSym0 a1627817219) l0 = AbsSym1 a1627817219 l0

type AbsSym1 t = Abs t Source #

data SignumSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun a1627817219 a1627817219 -> *) (SignumSym0 a1627817219) Source #
Methods suppressUnusedWarnings :: Proxy (SignumSym0 a1627817219) t -> () Source #
type Apply a1627817219 a1627817219 (SignumSym0 a1627817219) l0 Source #
type Apply a1627817219 a1627817219 (SignumSym0 a1627817219) l0 = SignumSym1 a1627817219 l0

type SignumSym1 t = Signum t Source #

data FromIntegerSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun Nat a1627817219 -> *) (FromIntegerSym0 a1627817219) Source #
Methods suppressUnusedWarnings :: Proxy (FromIntegerSym0 a1627817219) t -> () Source #
type Apply Nat k2 (FromIntegerSym0 k2) l0 Source #
type Apply Nat k2 (FromIntegerSym0 k2) l0 = FromIntegerSym1 k2 l0

type FromIntegerSym1 t = FromInteger t Source #

data SubtractSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun a1627819601 (TyFun a1627819601 a1627819601 -> Type) -> *) (SubtractSym0 a1627819601) Source #
Methods suppressUnusedWarnings :: Proxy (SubtractSym0 a1627819601) t -> () Source #
type Apply a1627819601 (TyFun a1627819601 a1627819601 -> Type) (SubtractSym0 a1627819601) l0 Source #
type Apply a1627819601 (TyFun a1627819601 a1627819601 -> Type) (SubtractSym0 a1627819601) l0 = SubtractSym1 a1627819601 l0

data SubtractSym1 l l Source #

Instances

SuppressUnusedWarnings (a1627819601 -> TyFun a1627819601 a1627819601 -> *) (SubtractSym1 a1627819601) Source #
Methods suppressUnusedWarnings :: Proxy (SubtractSym1 a1627819601) t -> () Source #
type Apply a1627819601 a1627819601 (SubtractSym1 a1627819601 l1) l0 Source #
type Apply a1627819601 a1627819601 (SubtractSym1 a1627819601 l1) l0 = SubtractSym2 a1627819601 l1 l0

type SubtractSym2 t t = Subtract t t Source #