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
Description
Defines and exports promoted and singleton versions of definitions from GHC.Num.
- class (kproxy ~ Proxy) => PNum kproxy where
- class SNum a where
- type family Subtract (a :: a) (a :: a) :: a where ...
- sSubtract :: forall t t. SNum a => Sing t -> Sing t -> Sing (Apply (Apply SubtractSym0 t) t :: a)
- data (:+$) l
- data l :+$$ l
- type (:+$$$) t t = (:+) t t
- data (:-$) l
- data l :-$$ l
- type (:-$$$) t t = (:-) t t
- data (:*$) l
- data l :*$$ l
- type (:*$$$) t t = (:*) t t
- data NegateSym0 l
- type NegateSym1 t = Negate t
- data AbsSym0 l
- type AbsSym1 t = Abs t
- data SignumSym0 l
- type SignumSym1 t = Signum t
- data FromIntegerSym0 l
- type FromIntegerSym1 t = FromInteger t
- data SubtractSym0 l
- data SubtractSym1 l l
- type SubtractSym2 t t = Subtract t t
Documentation
Minimal complete definition
Methods
(%:+) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:+$) t) t :: a) infixl 6 #
(%:-) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:-$) t) t :: a) infixl 6 #
(%:*) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:*$) t) t :: a) infixl 7 #
sNegate :: forall t. Sing t -> Sing (Apply NegateSym0 t :: a) #
sAbs :: forall t. Sing t -> Sing (Apply AbsSym0 t :: a) #
sSignum :: forall t. Sing t -> Sing (Apply SignumSym0 t :: a) #
sFromInteger :: forall t. Sing t -> Sing (Apply FromIntegerSym0 t :: a) #
(%:-) :: forall t t. (Apply (Apply (:-$) t) t ~ Apply (Apply TFHelper_6989586621679869182Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (:-$) t) t :: a) infixl 6 #
sNegate :: forall t. (Apply NegateSym0 t ~ Apply Negate_6989586621679869197Sym0 t) => Sing t -> Sing (Apply NegateSym0 t :: a) #
Defunctionalization symbols
data NegateSym0 l #
Instances
SuppressUnusedWarnings (TyFun a6989586621679869121 a6989586621679869121 -> *) (NegateSym0 a6989586621679869121) # | |
type Apply a6989586621679869121 a6989586621679869121 (NegateSym0 a6989586621679869121) l0 # | |
type NegateSym1 t = Negate t #
data SignumSym0 l #
Instances
SuppressUnusedWarnings (TyFun a6989586621679869121 a6989586621679869121 -> *) (SignumSym0 a6989586621679869121) # | |
type Apply a6989586621679869121 a6989586621679869121 (SignumSym0 a6989586621679869121) l0 # | |
type SignumSym1 t = Signum t #
data FromIntegerSym0 l #
Instances
SuppressUnusedWarnings (TyFun Nat a6989586621679869121 -> *) (FromIntegerSym0 a6989586621679869121) # | |
type Apply Nat k2 (FromIntegerSym0 k2) l0 # | |
type FromIntegerSym1 t = FromInteger t #
data SubtractSym0 l #
Instances
SuppressUnusedWarnings (TyFun a6989586621679871437 (TyFun a6989586621679871437 a6989586621679871437 -> Type) -> *) (SubtractSym0 a6989586621679871437) # | |
type Apply a6989586621679871437 (TyFun a6989586621679871437 a6989586621679871437 -> Type) (SubtractSym0 a6989586621679871437) l0 # | |
data SubtractSym1 l l #
Instances
SuppressUnusedWarnings (a6989586621679871437 -> TyFun a6989586621679871437 a6989586621679871437 -> *) (SubtractSym1 a6989586621679871437) # | |
type Apply a6989586621679871437 a6989586621679871437 (SubtractSym1 a6989586621679871437 l0) l1 # | |
type SubtractSym2 t t = Subtract t t #