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 PBounded (a :: Type) where
- class SBounded a where
- class PEnum (a :: Type) 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 :: TyFun a6989586621679673920 a6989586621679673920)
- type SuccSym1 (t :: a6989586621679673920) = Succ t
- data PredSym0 (l :: TyFun a6989586621679673920 a6989586621679673920)
- type PredSym1 (t :: a6989586621679673920) = Pred t
- data ToEnumSym0 (l :: TyFun Nat a6989586621679673920)
- type ToEnumSym1 (t :: Nat) = ToEnum t
- data FromEnumSym0 (l :: TyFun a6989586621679673920 Nat)
- type FromEnumSym1 (t :: a6989586621679673920) = FromEnum t
- data EnumFromToSym0 (l :: TyFun a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type))
- data EnumFromToSym1 (l :: a6989586621679673920) (l :: TyFun a6989586621679673920 [a6989586621679673920])
- type EnumFromToSym2 (t :: a6989586621679673920) (t :: a6989586621679673920) = EnumFromTo t t
- data EnumFromThenToSym0 (l :: TyFun a6989586621679673920 (TyFun a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type) -> Type))
- data EnumFromThenToSym1 (l :: a6989586621679673920) (l :: TyFun a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type))
- data EnumFromThenToSym2 (l :: a6989586621679673920) (l :: a6989586621679673920) (l :: TyFun a6989586621679673920 [a6989586621679673920])
- type EnumFromThenToSym3 (t :: a6989586621679673920) (t :: a6989586621679673920) (t :: a6989586621679673920) = EnumFromThenTo t t t
Documentation
Instances
SBounded Bool # | |
SBounded Ordering # | |
SBounded () # | |
(SBounded a, SBounded b) => SBounded (a, b) # | |
(SBounded a, SBounded b, SBounded c) => SBounded (a, b, c) # | |
(SBounded a, SBounded b, SBounded c, SBounded d) => SBounded (a, b, c, d) # | |
(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e) => SBounded (a, b, c, d, e) # | |
(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e, SBounded f) => SBounded (a, b, c, d, e, f) # | |
(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e, SBounded f, SBounded g) => SBounded (a, b, c, d, e, f, g) # | |
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 :: a). Sing t -> Sing (Apply SuccSym0 t :: a) #
sPred :: forall (t :: a). Sing t -> Sing (Apply PredSym0 t :: a) #
sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t :: a) #
sFromEnum :: forall (t :: a). Sing t -> Sing (Apply FromEnumSym0 t :: Nat) #
sEnumFromTo :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t :: [a]) #
sEnumFromThenTo :: forall (t :: a) (t :: a) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a]) #
sSucc :: forall (t :: a). ((Apply SuccSym0 t :: a) ~ Apply Succ_6989586621679674511Sym0 t) => Sing t -> Sing (Apply SuccSym0 t :: a) #
sPred :: forall (t :: a). ((Apply PredSym0 t :: a) ~ Apply Pred_6989586621679674524Sym0 t) => Sing t -> Sing (Apply PredSym0 t :: a) #
sEnumFromTo :: forall (t :: a) (t :: a). ((Apply (Apply EnumFromToSym0 t) t :: [a]) ~ Apply (Apply EnumFromTo_6989586621679674542Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t :: [a]) #
sEnumFromThenTo :: forall (t :: a) (t :: a) (t :: a). ((Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a]) ~ Apply (Apply (Apply EnumFromThenTo_6989586621679674572Sym0 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 :: TyFun Nat a6989586621679673920) #
Instances
SuppressUnusedWarnings (TyFun Nat a6989586621679673920 -> *) (ToEnumSym0 a6989586621679673920) # | |
type Apply Nat k2 (ToEnumSym0 k2) l # | |
type ToEnumSym1 (t :: Nat) = ToEnum t #
data FromEnumSym0 (l :: TyFun a6989586621679673920 Nat) #
Instances
SuppressUnusedWarnings (TyFun a6989586621679673920 Nat -> *) (FromEnumSym0 a6989586621679673920) # | |
type Apply a Nat (FromEnumSym0 a) l # | |
type FromEnumSym1 (t :: a6989586621679673920) = FromEnum t #
data EnumFromToSym0 (l :: TyFun a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type)) #
Instances
SuppressUnusedWarnings (TyFun a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type) -> *) (EnumFromToSym0 a6989586621679673920) # | |
type Apply a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type) (EnumFromToSym0 a6989586621679673920) l # | |
data EnumFromToSym1 (l :: a6989586621679673920) (l :: TyFun a6989586621679673920 [a6989586621679673920]) #
Instances
SuppressUnusedWarnings (a6989586621679673920 -> TyFun a6989586621679673920 [a6989586621679673920] -> *) (EnumFromToSym1 a6989586621679673920) # | |
type Apply a [a] (EnumFromToSym1 a l1) l2 # | |
type EnumFromToSym2 (t :: a6989586621679673920) (t :: a6989586621679673920) = EnumFromTo t t #
data EnumFromThenToSym0 (l :: TyFun a6989586621679673920 (TyFun a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type) -> Type)) #
Instances
SuppressUnusedWarnings (TyFun a6989586621679673920 (TyFun a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type) -> Type) -> *) (EnumFromThenToSym0 a6989586621679673920) # | |
type Apply a6989586621679673920 (TyFun a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type) -> Type) (EnumFromThenToSym0 a6989586621679673920) l # | |
data EnumFromThenToSym1 (l :: a6989586621679673920) (l :: TyFun a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type)) #
Instances
SuppressUnusedWarnings (a6989586621679673920 -> TyFun a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type) -> *) (EnumFromThenToSym1 a6989586621679673920) # | |
type Apply a6989586621679673920 (TyFun a6989586621679673920 [a6989586621679673920] -> Type) (EnumFromThenToSym1 a6989586621679673920 l1) l2 # | |
data EnumFromThenToSym2 (l :: a6989586621679673920) (l :: a6989586621679673920) (l :: TyFun a6989586621679673920 [a6989586621679673920]) #
Instances
SuppressUnusedWarnings (a6989586621679673920 -> a6989586621679673920 -> TyFun a6989586621679673920 [a6989586621679673920] -> *) (EnumFromThenToSym2 a6989586621679673920) # | |
type Apply a [a] (EnumFromThenToSym2 a l1 l2) l3 # | |
type EnumFromThenToSym3 (t :: a6989586621679673920) (t :: a6989586621679673920) (t :: a6989586621679673920) = EnumFromThenTo t t t #