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

class PBounded (a :: Type) where
- type MinBound :: a
- type MaxBound :: a
class SBounded a where
- sMinBound :: Sing (MinBoundSym0 :: a)
- sMaxBound :: Sing (MaxBoundSym0 :: a)
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
- 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])
type MinBoundSym0 = MinBound
type MaxBoundSym0 = MaxBound
data SuccSym0 :: forall a6989586621679761742. (~>) a6989586621679761742 a6989586621679761742
type SuccSym1 (arg6989586621679762026 :: a6989586621679761742) = Succ arg6989586621679762026
data PredSym0 :: forall a6989586621679761742. (~>) a6989586621679761742 a6989586621679761742
type PredSym1 (arg6989586621679762028 :: a6989586621679761742) = Pred arg6989586621679762028
data ToEnumSym0 :: forall a6989586621679761742. (~>) Nat a6989586621679761742
type ToEnumSym1 (arg6989586621679762030 :: Nat) = ToEnum arg6989586621679762030
data FromEnumSym0 :: forall a6989586621679761742. (~>) a6989586621679761742 Nat
type FromEnumSym1 (arg6989586621679762032 :: a6989586621679761742) = FromEnum arg6989586621679762032
data EnumFromToSym0 :: forall a6989586621679761742. (~>) a6989586621679761742 ((~>) a6989586621679761742 [a6989586621679761742])
data EnumFromToSym1 (arg6989586621679762034 :: a6989586621679761742) :: (~>) a6989586621679761742 [a6989586621679761742]
type EnumFromToSym2 (arg6989586621679762034 :: a6989586621679761742) (arg6989586621679762035 :: a6989586621679761742) = EnumFromTo arg6989586621679762034 arg6989586621679762035
data EnumFromThenToSym0 :: forall a6989586621679761742. (~>) a6989586621679761742 ((~>) a6989586621679761742 ((~>) a6989586621679761742 [a6989586621679761742]))
data EnumFromThenToSym1 (arg6989586621679762038 :: a6989586621679761742) :: (~>) a6989586621679761742 ((~>) a6989586621679761742 [a6989586621679761742])
data EnumFromThenToSym2 (arg6989586621679762038 :: a6989586621679761742) (arg6989586621679762039 :: a6989586621679761742) :: (~>) a6989586621679761742 [a6989586621679761742]
type EnumFromThenToSym3 (arg6989586621679762038 :: a6989586621679761742) (arg6989586621679762039 :: a6989586621679761742) (arg6989586621679762040 :: a6989586621679761742) = EnumFromThenTo arg6989586621679762038 arg6989586621679762039 arg6989586621679762040

Documentation

class PBounded (a :: Type) #

Associated Types

type MinBound :: a #

type MaxBound :: a #

Instances

PBounded Bool #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a # type MaxBound :: a #
PBounded Ordering #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a # type MaxBound :: a #
PBounded () #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a # type MaxBound :: a #
PBounded All #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a # type MaxBound :: a #
PBounded Any #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (Min a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (Max a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (First a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (Last a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (WrappedMonoid m) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (Identity a) #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (Dual a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (Sum a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (Product a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (a, b) #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (a, b, c) #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (a, b, c, d) #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (a, b, c, d, e) #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (a, b, c, d, e, f) #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a # type MaxBound :: a #
PBounded (a, b, c, d, e, f, g) #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a # type MaxBound :: a #

class SBounded a where #

Methods

sMinBound :: Sing (MinBoundSym0 :: a) #

sMaxBound :: Sing (MaxBoundSym0 :: a) #

Instances

SBounded Bool #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded Ordering #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded () #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded Bool => SBounded All #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded Bool => SBounded Any #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded a => SBounded (Min a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded a => SBounded (Max a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded a => SBounded (First a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded a => SBounded (Last a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded m => SBounded (WrappedMonoid m) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded a => SBounded (Identity a) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded a => SBounded (Dual a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded a => SBounded (Sum a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded a => SBounded (Product a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
(SBounded a, SBounded b) => SBounded (a, b) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
(SBounded a, SBounded b, SBounded c) => SBounded (a, b, c) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SBounded a => SBounded (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
(SBounded a, SBounded b, SBounded c, SBounded d) => SBounded (a, b, c, d) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e) => SBounded (a, b, c, d, e) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e, SBounded f) => SBounded (a, b, c, d, e, f) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e, SBounded f, SBounded g) => SBounded (a, b, c, d, e, f, g) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #

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 #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg :: [a] # type EnumFromThenTo arg arg arg :: [a] #
PEnum Ordering #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg :: [a] # type EnumFromThenTo arg arg arg :: [a] #
PEnum Nat #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg :: [a] # type EnumFromThenTo arg arg arg :: [a] #
PEnum () #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg :: [a] # type EnumFromThenTo arg arg arg :: [a] #
PEnum (Min a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg :: [a] # type EnumFromThenTo arg arg arg :: [a] #
PEnum (Max a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg :: [a] # type EnumFromThenTo arg arg arg :: [a] #
PEnum (First a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg :: [a] # type EnumFromThenTo arg arg arg :: [a] #
PEnum (Last a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg :: [a] # type EnumFromThenTo arg arg arg :: [a] #
PEnum (WrappedMonoid a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg :: [a] # type EnumFromThenTo arg arg arg :: [a] #
PEnum (Identity a) #
Instance details Defined in Data.Singletons.Prelude.Identity Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg :: [a] # type EnumFromThenTo arg arg arg :: [a] #
PEnum (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: 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_6989586621679762056Sym0 t => Sing t -> Sing (Apply SuccSym0 t :: a) #

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

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

Instances

SEnum Bool #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #
SEnum Ordering #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #
SEnum Nat #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #
SEnum () #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #
SEnum a => SEnum (Min a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #
SEnum a => SEnum (Max a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #
SEnum a => SEnum (First a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #
SEnum a => SEnum (Last a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #
SEnum a => SEnum (WrappedMonoid a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #
SEnum a => SEnum (Identity a) #
Instance details Defined in Data.Singletons.Prelude.Identity Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #
SEnum a => SEnum (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #

Defunctionalization symbols

type MinBoundSym0 = MinBound #

type MaxBoundSym0 = MaxBound #

data SuccSym0 :: forall a6989586621679761742. (~>) a6989586621679761742 a6989586621679761742 #

Instances

SEnum a => SingI (SuccSym0 :: TyFun a a -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing SuccSym0 #
SuppressUnusedWarnings (SuccSym0 :: TyFun a6989586621679761742 a6989586621679761742 -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
type Apply (SuccSym0 :: TyFun a a -> Type) (arg6989586621679762026 :: a) #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (SuccSym0 :: TyFun a a -> Type) (arg6989586621679762026 :: a) = Succ arg6989586621679762026

type SuccSym1 (arg6989586621679762026 :: a6989586621679761742) = Succ arg6989586621679762026 #

data PredSym0 :: forall a6989586621679761742. (~>) a6989586621679761742 a6989586621679761742 #

Instances

SEnum a => SingI (PredSym0 :: TyFun a a -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing PredSym0 #
SuppressUnusedWarnings (PredSym0 :: TyFun a6989586621679761742 a6989586621679761742 -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
type Apply (PredSym0 :: TyFun a a -> Type) (arg6989586621679762028 :: a) #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (PredSym0 :: TyFun a a -> Type) (arg6989586621679762028 :: a) = Pred arg6989586621679762028

type PredSym1 (arg6989586621679762028 :: a6989586621679761742) = Pred arg6989586621679762028 #

data ToEnumSym0 :: forall a6989586621679761742. (~>) Nat a6989586621679761742 #

Instances

SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing ToEnumSym0 #
SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a6989586621679761742 -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (arg6989586621679762030 :: Nat) #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (arg6989586621679762030 :: Nat) = (ToEnum arg6989586621679762030 :: k2)

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

data FromEnumSym0 :: forall a6989586621679761742. (~>) a6989586621679761742 Nat #

Instances

SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing FromEnumSym0 #
SuppressUnusedWarnings (FromEnumSym0 :: TyFun a6989586621679761742 Nat -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679762032 :: a) #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (arg6989586621679762032 :: a) = FromEnum arg6989586621679762032

type FromEnumSym1 (arg6989586621679762032 :: a6989586621679761742) = FromEnum arg6989586621679762032 #

data EnumFromToSym0 :: forall a6989586621679761742. (~>) a6989586621679761742 ((~>) a6989586621679761742 [a6989586621679761742]) #

Instances

SEnum a => SingI (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EnumFromToSym0 #
SuppressUnusedWarnings (EnumFromToSym0 :: TyFun a6989586621679761742 (a6989586621679761742 ~> [a6989586621679761742]) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
type Apply (EnumFromToSym0 :: TyFun a6989586621679761742 (a6989586621679761742 ~> [a6989586621679761742]) -> Type) (arg6989586621679762034 :: a6989586621679761742) #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromToSym0 :: TyFun a6989586621679761742 (a6989586621679761742 ~> [a6989586621679761742]) -> Type) (arg6989586621679762034 :: a6989586621679761742) = EnumFromToSym1 arg6989586621679762034

data EnumFromToSym1 (arg6989586621679762034 :: a6989586621679761742) :: (~>) a6989586621679761742 [a6989586621679761742] #

Instances

(SEnum a, SingI d) => SingI (EnumFromToSym1 d :: TyFun a [a] -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromToSym1 d) #
SuppressUnusedWarnings (EnumFromToSym1 arg6989586621679762034 :: TyFun a6989586621679761742 [a6989586621679761742] -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
type Apply (EnumFromToSym1 arg6989586621679762034 :: TyFun a [a] -> Type) (arg6989586621679762035 :: a) #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromToSym1 arg6989586621679762034 :: TyFun a [a] -> Type) (arg6989586621679762035 :: a) = EnumFromTo arg6989586621679762034 arg6989586621679762035

type EnumFromToSym2 (arg6989586621679762034 :: a6989586621679761742) (arg6989586621679762035 :: a6989586621679761742) = EnumFromTo arg6989586621679762034 arg6989586621679762035 #

data EnumFromThenToSym0 :: forall a6989586621679761742. (~>) a6989586621679761742 ((~>) a6989586621679761742 ((~>) a6989586621679761742 [a6989586621679761742])) #

Instances

SEnum a => SingI (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EnumFromThenToSym0 #
SuppressUnusedWarnings (EnumFromThenToSym0 :: TyFun a6989586621679761742 (a6989586621679761742 ~> (a6989586621679761742 ~> [a6989586621679761742])) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
type Apply (EnumFromThenToSym0 :: TyFun a6989586621679761742 (a6989586621679761742 ~> (a6989586621679761742 ~> [a6989586621679761742])) -> Type) (arg6989586621679762038 :: a6989586621679761742) #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromThenToSym0 :: TyFun a6989586621679761742 (a6989586621679761742 ~> (a6989586621679761742 ~> [a6989586621679761742])) -> Type) (arg6989586621679762038 :: a6989586621679761742) = EnumFromThenToSym1 arg6989586621679762038

data EnumFromThenToSym1 (arg6989586621679762038 :: a6989586621679761742) :: (~>) a6989586621679761742 ((~>) a6989586621679761742 [a6989586621679761742]) #

Instances

(SEnum a, SingI d) => SingI (EnumFromThenToSym1 d :: TyFun a (a ~> [a]) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromThenToSym1 d) #
SuppressUnusedWarnings (EnumFromThenToSym1 arg6989586621679762038 :: TyFun a6989586621679761742 (a6989586621679761742 ~> [a6989586621679761742]) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
type Apply (EnumFromThenToSym1 arg6989586621679762038 :: TyFun a6989586621679761742 (a6989586621679761742 ~> [a6989586621679761742]) -> Type) (arg6989586621679762039 :: a6989586621679761742) #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromThenToSym1 arg6989586621679762038 :: TyFun a6989586621679761742 (a6989586621679761742 ~> [a6989586621679761742]) -> Type) (arg6989586621679762039 :: a6989586621679761742) = EnumFromThenToSym2 arg6989586621679762038 arg6989586621679762039

data EnumFromThenToSym2 (arg6989586621679762038 :: a6989586621679761742) (arg6989586621679762039 :: a6989586621679761742) :: (~>) a6989586621679761742 [a6989586621679761742] #

Instances

(SEnum a, SingI d1, SingI d2) => SingI (EnumFromThenToSym2 d1 d2 :: TyFun a [a] -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromThenToSym2 d1 d2) #
SuppressUnusedWarnings (EnumFromThenToSym2 arg6989586621679762039 arg6989586621679762038 :: TyFun a6989586621679761742 [a6989586621679761742] -> Type) #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
type Apply (EnumFromThenToSym2 arg6989586621679762039 arg6989586621679762038 :: TyFun a [a] -> Type) (arg6989586621679762040 :: a) #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromThenToSym2 arg6989586621679762039 arg6989586621679762038 :: TyFun a [a] -> Type) (arg6989586621679762040 :: a) = EnumFromThenTo arg6989586621679762039 arg6989586621679762038 arg6989586621679762040

type EnumFromThenToSym3 (arg6989586621679762038 :: a6989586621679761742) (arg6989586621679762039 :: a6989586621679761742) (arg6989586621679762040 :: a6989586621679761742) = EnumFromThenTo arg6989586621679762038 arg6989586621679762039 arg6989586621679762040 #