Copyright | (C) 2014 Jan Stolarek Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Jan Stolarek (jan.stolarek@p.lodz.pl) |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Data.Singletons.Prelude.Enum
Contents
- class (kproxy ~ Proxy) => PBounded kproxy where
- class SBounded a where
- class (kproxy ~ Proxy) => PEnum kproxy where
- type Succ (arg :: a) :: a
- type Pred (arg :: a) :: a
- type ToEnum (arg :: Nat) :: a
- type FromEnum (arg :: a) :: Nat
- type EnumFromTo (arg :: a) (arg :: a) :: [a]
- type EnumFromThenTo (arg :: a) (arg :: a) (arg :: a) :: [a]
- class SEnum a where
- type MinBoundSym0 = MinBound
- type MaxBoundSym0 = MaxBound
- data SuccSym0 l
- type SuccSym1 t = Succ t
- data PredSym0 l
- type PredSym1 t = Pred t
- data ToEnumSym0 l
- type ToEnumSym1 t = ToEnum t
- data FromEnumSym0 l
- type FromEnumSym1 t = FromEnum t
- data EnumFromToSym0 l
- data EnumFromToSym1 l l
- type EnumFromToSym2 t t = EnumFromTo t t
- data EnumFromThenToSym0 l
- data EnumFromThenToSym1 l l
- data EnumFromThenToSym2 l l l
- type EnumFromThenToSym3 t t t = EnumFromThenTo t t t
Documentation
class (kproxy ~ Proxy) => PBounded kproxy #
Instances
PBounded Bool (Proxy * Bool) # | |
PBounded Ordering (Proxy * Ordering) # | |
PBounded () (Proxy * ()) # | |
PBounded (a0, b0) (Proxy * (a0, b0)) # | |
PBounded (a0, b0, c0) (Proxy * (a0, b0, c0)) # | |
PBounded (a0, b0, c0, d0) (Proxy * (a0, b0, c0, d0)) # | |
PBounded (a0, b0, c0, d0, e0) (Proxy * (a0, b0, c0, d0, e0)) # | |
PBounded (a0, b0, c0, d0, e0, f0) (Proxy * (a0, b0, c0, d0, e0, f0)) # | |
PBounded (a0, b0, c0, d0, e0, f0, g0) (Proxy * (a0, b0, c0, d0, e0, f0, g0)) # | |
Instances
SBounded Bool # | |
SBounded Ordering # | |
SBounded () # | |
(SBounded a0, SBounded b0) => SBounded (a0, b0) # | |
(SBounded a0, SBounded b0, SBounded c0) => SBounded (a0, b0, c0) # | |
(SBounded a0, SBounded b0, SBounded c0, SBounded d0) => SBounded (a0, b0, c0, d0) # | |
(SBounded a0, SBounded b0, SBounded c0, SBounded d0, SBounded e0) => SBounded (a0, b0, c0, d0, e0) # | |
(SBounded a0, SBounded b0, SBounded c0, SBounded d0, SBounded e0, SBounded f0) => SBounded (a0, b0, c0, d0, e0, f0) # | |
(SBounded a0, SBounded b0, SBounded c0, SBounded d0, SBounded e0, SBounded f0, SBounded g0) => SBounded (a0, b0, c0, d0, e0, f0, g0) # | |
class (kproxy ~ Proxy) => PEnum kproxy #
Associated Types
type ToEnum (arg :: Nat) :: a #
type FromEnum (arg :: a) :: Nat #
type EnumFromTo (arg :: a) (arg :: a) :: [a] #
type EnumFromThenTo (arg :: a) (arg :: a) (arg :: a) :: [a] #
Methods
sSucc :: forall t. Sing t -> Sing (Apply SuccSym0 t :: a) #
sPred :: forall t. Sing t -> Sing (Apply PredSym0 t :: a) #
sToEnum :: forall t. Sing t -> Sing (Apply ToEnumSym0 t :: a) #
sFromEnum :: forall t. Sing t -> Sing (Apply FromEnumSym0 t :: Nat) #
sEnumFromTo :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t :: [a]) #
sEnumFromThenTo :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a]) #
sSucc :: forall t. (Apply SuccSym0 t ~ Apply Succ_6989586621679883581Sym0 t) => Sing t -> Sing (Apply SuccSym0 t :: a) #
sPred :: forall t. (Apply PredSym0 t ~ Apply Pred_6989586621679883594Sym0 t) => Sing t -> Sing (Apply PredSym0 t :: a) #
sEnumFromTo :: forall t t. (Apply (Apply EnumFromToSym0 t) t ~ Apply (Apply EnumFromTo_6989586621679883612Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t :: [a]) #
sEnumFromThenTo :: forall t t t. (Apply (Apply (Apply EnumFromThenToSym0 t) t) t ~ Apply (Apply (Apply EnumFromThenTo_6989586621679883642Sym0 t) t) t) => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a]) #
Defunctionalization symbols
type MinBoundSym0 = MinBound #
type MaxBoundSym0 = MaxBound #
data ToEnumSym0 l #
Instances
SuppressUnusedWarnings (TyFun Nat a6989586621679883002 -> *) (ToEnumSym0 a6989586621679883002) # | |
type Apply Nat k2 (ToEnumSym0 k2) l0 # | |
type ToEnumSym1 t = ToEnum t #
data FromEnumSym0 l #
Instances
SuppressUnusedWarnings (TyFun a6989586621679883002 Nat -> *) (FromEnumSym0 a6989586621679883002) # | |
type Apply a6989586621679883002 Nat (FromEnumSym0 a6989586621679883002) l0 # | |
type FromEnumSym1 t = FromEnum t #
data EnumFromToSym0 l #
Instances
SuppressUnusedWarnings (TyFun a6989586621679883002 (TyFun a6989586621679883002 [a6989586621679883002] -> Type) -> *) (EnumFromToSym0 a6989586621679883002) # | |
type Apply a6989586621679883002 (TyFun a6989586621679883002 [a6989586621679883002] -> Type) (EnumFromToSym0 a6989586621679883002) l0 # | |
data EnumFromToSym1 l l #
Instances
SuppressUnusedWarnings (a6989586621679883002 -> TyFun a6989586621679883002 [a6989586621679883002] -> *) (EnumFromToSym1 a6989586621679883002) # | |
type Apply a6989586621679883002 [a6989586621679883002] (EnumFromToSym1 a6989586621679883002 l0) l1 # | |
type EnumFromToSym2 t t = EnumFromTo t t #
data EnumFromThenToSym0 l #
Instances
SuppressUnusedWarnings (TyFun a6989586621679883002 (TyFun a6989586621679883002 (TyFun a6989586621679883002 [a6989586621679883002] -> Type) -> Type) -> *) (EnumFromThenToSym0 a6989586621679883002) # | |
type Apply a6989586621679883002 (TyFun a6989586621679883002 (TyFun a6989586621679883002 [a6989586621679883002] -> Type) -> Type) (EnumFromThenToSym0 a6989586621679883002) l0 # | |
data EnumFromThenToSym1 l l #
Instances
SuppressUnusedWarnings (a6989586621679883002 -> TyFun a6989586621679883002 (TyFun a6989586621679883002 [a6989586621679883002] -> Type) -> *) (EnumFromThenToSym1 a6989586621679883002) # | |
type Apply a6989586621679883002 (TyFun a6989586621679883002 [a6989586621679883002] -> Type) (EnumFromThenToSym1 a6989586621679883002 l0) l1 # | |
data EnumFromThenToSym2 l l l #
Instances
SuppressUnusedWarnings (a6989586621679883002 -> a6989586621679883002 -> TyFun a6989586621679883002 [a6989586621679883002] -> *) (EnumFromThenToSym2 a6989586621679883002) # | |
type Apply a6989586621679883002 [a6989586621679883002] (EnumFromThenToSym2 a6989586621679883002 l1 l0) l2 # | |
type EnumFromThenToSym3 t t t = EnumFromThenTo t t t #