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

Defunctionalization symbols

Description

Defines the promoted and singleton version of Bounded, PBounded and SBounded

Synopsis

Documentation

class PBounded (a :: Type) #

Associated Types

type MinBound :: a #

type MaxBound :: a #

Instances

PBounded Bool #
Associated Types type MinBound Bool :: a # type MaxBound Bool :: a #
PBounded Ordering #
Associated Types type MinBound Ordering :: a # type MaxBound Ordering :: a #
PBounded () #
Associated Types type MinBound () :: a # type MaxBound () :: a #
PBounded (a, b) #
Associated Types type MinBound (a, b) :: a # type MaxBound (a, b) :: a #
PBounded (a, b, c) #
Associated Types type MinBound (a, b, c) :: a # type MaxBound (a, b, c) :: a #
PBounded (a, b, c, d) #
Associated Types type MinBound (a, b, c, d) :: a # type MaxBound (a, b, c, d) :: a #
PBounded (a, b, c, d, e) #
Associated Types type MinBound (a, b, c, d, e) :: a # type MaxBound (a, b, c, d, e) :: a #
PBounded (a, b, c, d, e, f) #
Associated Types type MinBound (a, b, c, d, e, f) :: a # type MaxBound (a, b, c, d, e, f) :: a #
PBounded (a, b, c, d, e, f, g) #
Associated Types type MinBound (a, b, c, d, e, f, g) :: a # type MaxBound (a, b, c, d, e, f, g) :: a #

class SBounded a where #

Minimal complete definition

sMinBound, sMaxBound

Methods

sMinBound :: Sing (MinBoundSym0 :: a) #

sMaxBound :: Sing (MaxBoundSym0 :: a) #

Instances

SBounded Bool #
Methods sMinBound :: Sing Bool (MinBoundSym0 Bool) # sMaxBound :: Sing Bool (MaxBoundSym0 Bool) #
SBounded Ordering #
Methods sMinBound :: Sing Ordering (MinBoundSym0 Ordering) # sMaxBound :: Sing Ordering (MaxBoundSym0 Ordering) #
SBounded () #
Methods sMinBound :: Sing () (MinBoundSym0 ()) # sMaxBound :: Sing () (MaxBoundSym0 ()) #
(SBounded a, SBounded b) => SBounded (a, b) #
Methods sMinBound :: Sing (a, b) (MinBoundSym0 (a, b)) # sMaxBound :: Sing (a, b) (MaxBoundSym0 (a, b)) #
(SBounded a, SBounded b, SBounded c) => SBounded (a, b, c) #
Methods sMinBound :: Sing (a, b, c) (MinBoundSym0 (a, b, c)) # sMaxBound :: Sing (a, b, c) (MaxBoundSym0 (a, b, c)) #
(SBounded a, SBounded b, SBounded c, SBounded d) => SBounded (a, b, c, d) #
Methods sMinBound :: Sing (a, b, c, d) (MinBoundSym0 (a, b, c, d)) # sMaxBound :: Sing (a, b, c, d) (MaxBoundSym0 (a, b, c, d)) #
(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e) => SBounded (a, b, c, d, e) #
Methods sMinBound :: Sing (a, b, c, d, e) (MinBoundSym0 (a, b, c, d, e)) # sMaxBound :: Sing (a, b, c, d, e) (MaxBoundSym0 (a, b, c, d, e)) #
(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e, SBounded f) => SBounded (a, b, c, d, e, f) #
Methods sMinBound :: Sing (a, b, c, d, e, f) (MinBoundSym0 (a, b, c, d, e, f)) # sMaxBound :: Sing (a, b, c, d, e, f) (MaxBoundSym0 (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) #
Methods sMinBound :: Sing (a, b, c, d, e, f, g) (MinBoundSym0 (a, b, c, d, e, f, g)) # sMaxBound :: Sing (a, b, c, d, e, f, g) (MaxBoundSym0 (a, b, c, d, e, f, g)) #

class PEnum (a :: Type) #

Associated Types

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] #

Instances

PEnum Bool #
Associated Types type Succ Bool (arg :: Bool) :: a # type Pred Bool (arg :: Bool) :: a # type ToEnum Bool (arg :: Nat) :: a # type FromEnum Bool (arg :: Bool) :: Nat # type EnumFromTo Bool (arg :: Bool) (arg :: Bool) :: [a] # type EnumFromThenTo Bool (arg :: Bool) (arg :: Bool) (arg :: Bool) :: [a] #
PEnum Ordering #
Associated Types type Succ Ordering (arg :: Ordering) :: a # type Pred Ordering (arg :: Ordering) :: a # type ToEnum Ordering (arg :: Nat) :: a # type FromEnum Ordering (arg :: Ordering) :: Nat # type EnumFromTo Ordering (arg :: Ordering) (arg :: Ordering) :: [a] # type EnumFromThenTo Ordering (arg :: Ordering) (arg :: Ordering) (arg :: Ordering) :: [a] #
PEnum Nat #
Associated Types type Succ Nat (arg :: Nat) :: a # type Pred Nat (arg :: Nat) :: a # type ToEnum Nat (arg :: Nat) :: a # type FromEnum Nat (arg :: Nat) :: Nat # type EnumFromTo Nat (arg :: Nat) (arg :: Nat) :: [a] # type EnumFromThenTo Nat (arg :: Nat) (arg :: Nat) (arg :: Nat) :: [a] #
PEnum () #
Associated Types type Succ () (arg :: ()) :: a # type Pred () (arg :: ()) :: a # type ToEnum () (arg :: Nat) :: a # type FromEnum () (arg :: ()) :: Nat # type EnumFromTo () (arg :: ()) (arg :: ()) :: [a] # type EnumFromThenTo () (arg :: ()) (arg :: ()) (arg :: ()) :: [a] #

class SEnum a where #

Minimal complete definition

sToEnum, sFromEnum

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_1628218572Sym0 t) => Sing t -> Sing (Apply SuccSym0 t :: a) #

sPred :: forall (t :: a). ((Apply PredSym0 t :: a) ~ Apply Pred_1628218585Sym0 t) => Sing t -> Sing (Apply PredSym0 t :: a) #

sEnumFromTo :: forall (t :: a) (t :: a). ((Apply (Apply EnumFromToSym0 t) t :: [a]) ~ Apply (Apply EnumFromTo_1628218603Sym0 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_1628218633Sym0 t) t) t) => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a]) #

Instances

SEnum Bool #
Methods sSucc :: Sing Bool t -> Sing Bool (Apply Bool Bool (SuccSym0 Bool) t) # sPred :: Sing Bool t -> Sing Bool (Apply Bool Bool (PredSym0 Bool) t) # sToEnum :: Sing Nat t -> Sing Bool (Apply Nat Bool (ToEnumSym0 Bool) t) # sFromEnum :: Sing Bool t -> Sing Nat (Apply Bool Nat (FromEnumSym0 Bool) t) # sEnumFromTo :: Sing Bool t -> Sing Bool t -> Sing [Bool] (Apply Bool [Bool] (Apply Bool (TyFun Bool [Bool] -> Type) (EnumFromToSym0 Bool) t) t) # sEnumFromThenTo :: Sing Bool t -> Sing Bool t -> Sing Bool t -> Sing [Bool] (Apply Bool [Bool] (Apply Bool (TyFun Bool [Bool] -> Type) (Apply Bool (TyFun Bool (TyFun Bool [Bool] -> Type) -> Type) (EnumFromThenToSym0 Bool) t) t) t) #
SEnum Ordering #
Methods sSucc :: Sing Ordering t -> Sing Ordering (Apply Ordering Ordering (SuccSym0 Ordering) t) # sPred :: Sing Ordering t -> Sing Ordering (Apply Ordering Ordering (PredSym0 Ordering) t) # sToEnum :: Sing Nat t -> Sing Ordering (Apply Nat Ordering (ToEnumSym0 Ordering) t) # sFromEnum :: Sing Ordering t -> Sing Nat (Apply Ordering Nat (FromEnumSym0 Ordering) t) # sEnumFromTo :: Sing Ordering t -> Sing Ordering t -> Sing [Ordering] (Apply Ordering [Ordering] (Apply Ordering (TyFun Ordering [Ordering] -> Type) (EnumFromToSym0 Ordering) t) t) # sEnumFromThenTo :: Sing Ordering t -> Sing Ordering t -> Sing Ordering t -> Sing [Ordering] (Apply Ordering [Ordering] (Apply Ordering (TyFun Ordering [Ordering] -> Type) (Apply Ordering (TyFun Ordering (TyFun Ordering [Ordering] -> Type) -> Type) (EnumFromThenToSym0 Ordering) t) t) t) #
SEnum Nat #
Methods sSucc :: Sing Nat t -> Sing Nat (Apply Nat Nat (SuccSym0 Nat) t) # sPred :: Sing Nat t -> Sing Nat (Apply Nat Nat (PredSym0 Nat) t) # sToEnum :: Sing Nat t -> Sing Nat (Apply Nat Nat (ToEnumSym0 Nat) t) # sFromEnum :: Sing Nat t -> Sing Nat (Apply Nat Nat (FromEnumSym0 Nat) t) # sEnumFromTo :: Sing Nat t -> Sing Nat t -> Sing [Nat] (Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (EnumFromToSym0 Nat) t) t) # sEnumFromThenTo :: Sing Nat t -> Sing Nat t -> Sing Nat t -> Sing [Nat] (Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (Apply Nat (TyFun Nat (TyFun Nat [Nat] -> Type) -> Type) (EnumFromThenToSym0 Nat) t) t) t) #
SEnum () #
Methods sSucc :: Sing () t -> Sing () (Apply () () (SuccSym0 ()) t) # sPred :: Sing () t -> Sing () (Apply () () (PredSym0 ()) t) # sToEnum :: Sing Nat t -> Sing () (Apply Nat () (ToEnumSym0 ()) t) # sFromEnum :: Sing () t -> Sing Nat (Apply () Nat (FromEnumSym0 ()) t) # sEnumFromTo :: Sing () t -> Sing () t -> Sing [()] (Apply () [()] (Apply () (TyFun () [()] -> Type) (EnumFromToSym0 ()) t) t) # sEnumFromThenTo :: Sing () t -> Sing () t -> Sing () t -> Sing [()] (Apply () [()] (Apply () (TyFun () [()] -> Type) (Apply () (TyFun () (TyFun () [()] -> Type) -> Type) (EnumFromThenToSym0 ()) t) t) t) #

Defunctionalization symbols

type MinBoundSym0 = MinBound #

type MaxBoundSym0 = MaxBound #

data SuccSym0 (l :: TyFun a1628217981 a1628217981) #

Instances

SuppressUnusedWarnings (TyFun a1628217981 a1628217981 -> *) (SuccSym0 a1628217981) #
Methods suppressUnusedWarnings :: Proxy (SuccSym0 a1628217981) t -> () #
type Apply a a (SuccSym0 a) l #
type Apply a a (SuccSym0 a) l = Succ a l

type SuccSym1 (t :: a1628217981) = Succ t #

data PredSym0 (l :: TyFun a1628217981 a1628217981) #

Instances

SuppressUnusedWarnings (TyFun a1628217981 a1628217981 -> *) (PredSym0 a1628217981) #
Methods suppressUnusedWarnings :: Proxy (PredSym0 a1628217981) t -> () #
type Apply a a (PredSym0 a) l #
type Apply a a (PredSym0 a) l = Pred a l

type PredSym1 (t :: a1628217981) = Pred t #

data ToEnumSym0 (l :: TyFun Nat a1628217981) #

Instances

SuppressUnusedWarnings (TyFun Nat a1628217981 -> *) (ToEnumSym0 a1628217981) #
Methods suppressUnusedWarnings :: Proxy (ToEnumSym0 a1628217981) t -> () #
type Apply Nat k2 (ToEnumSym0 k2) l #
type Apply Nat k2 (ToEnumSym0 k2) l = ToEnum k2 l

type ToEnumSym1 (t :: Nat) = ToEnum t #

data FromEnumSym0 (l :: TyFun a1628217981 Nat) #

Instances

SuppressUnusedWarnings (TyFun a1628217981 Nat -> *) (FromEnumSym0 a1628217981) #
Methods suppressUnusedWarnings :: Proxy (FromEnumSym0 a1628217981) t -> () #
type Apply a Nat (FromEnumSym0 a) l #
type Apply a Nat (FromEnumSym0 a) l = FromEnum a l

type FromEnumSym1 (t :: a1628217981) = FromEnum t #

data EnumFromToSym0 (l :: TyFun a1628217981 (TyFun a1628217981 [a1628217981] -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a1628217981 (TyFun a1628217981 [a1628217981] -> Type) -> *) (EnumFromToSym0 a1628217981) #
Methods suppressUnusedWarnings :: Proxy (EnumFromToSym0 a1628217981) t -> () #
type Apply a1628217981 (TyFun a1628217981 [a1628217981] -> Type) (EnumFromToSym0 a1628217981) l #
type Apply a1628217981 (TyFun a1628217981 [a1628217981] -> Type) (EnumFromToSym0 a1628217981) l = EnumFromToSym1 a1628217981 l

data EnumFromToSym1 (l :: a1628217981) (l :: TyFun a1628217981 [a1628217981]) #

Instances

SuppressUnusedWarnings (a1628217981 -> TyFun a1628217981 [a1628217981] -> *) (EnumFromToSym1 a1628217981) #
Methods suppressUnusedWarnings :: Proxy (EnumFromToSym1 a1628217981) t -> () #
type Apply a [a] (EnumFromToSym1 a l1) l2 #
type Apply a [a] (EnumFromToSym1 a l1) l2 = EnumFromTo a l1 l2

type EnumFromToSym2 (t :: a1628217981) (t :: a1628217981) = EnumFromTo t t #

data EnumFromThenToSym0 (l :: TyFun a1628217981 (TyFun a1628217981 (TyFun a1628217981 [a1628217981] -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a1628217981 (TyFun a1628217981 (TyFun a1628217981 [a1628217981] -> Type) -> Type) -> *) (EnumFromThenToSym0 a1628217981) #
Methods suppressUnusedWarnings :: Proxy (EnumFromThenToSym0 a1628217981) t -> () #
type Apply a1628217981 (TyFun a1628217981 (TyFun a1628217981 [a1628217981] -> Type) -> Type) (EnumFromThenToSym0 a1628217981) l #
type Apply a1628217981 (TyFun a1628217981 (TyFun a1628217981 [a1628217981] -> Type) -> Type) (EnumFromThenToSym0 a1628217981) l = EnumFromThenToSym1 a1628217981 l

data EnumFromThenToSym1 (l :: a1628217981) (l :: TyFun a1628217981 (TyFun a1628217981 [a1628217981] -> Type)) #

Instances

SuppressUnusedWarnings (a1628217981 -> TyFun a1628217981 (TyFun a1628217981 [a1628217981] -> Type) -> *) (EnumFromThenToSym1 a1628217981) #
Methods suppressUnusedWarnings :: Proxy (EnumFromThenToSym1 a1628217981) t -> () #
type Apply a1628217981 (TyFun a1628217981 [a1628217981] -> Type) (EnumFromThenToSym1 a1628217981 l1) l2 #
type Apply a1628217981 (TyFun a1628217981 [a1628217981] -> Type) (EnumFromThenToSym1 a1628217981 l1) l2 = EnumFromThenToSym2 a1628217981 l1 l2

data EnumFromThenToSym2 (l :: a1628217981) (l :: a1628217981) (l :: TyFun a1628217981 [a1628217981]) #

Instances

SuppressUnusedWarnings (a1628217981 -> a1628217981 -> TyFun a1628217981 [a1628217981] -> *) (EnumFromThenToSym2 a1628217981) #
Methods suppressUnusedWarnings :: Proxy (EnumFromThenToSym2 a1628217981) t -> () #
type Apply a [a] (EnumFromThenToSym2 a l1 l2) l3 #
type Apply a [a] (EnumFromThenToSym2 a l1 l2) l3 = EnumFromThenTo a l1 l2 l3

type EnumFromThenToSym3 (t :: a1628217981) (t :: a1628217981) (t :: a1628217981) = EnumFromThenTo t t t #