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