Data.Singletons.Prelude.Enum

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

Documentation

class (kproxy ~ Proxy) => PBounded kproxy

Associated Types

type MinBound :: a

type MaxBound :: a

Instances

PBounded Bool (Proxy * Bool)

Associated Types

type MinBound (Proxy * Bool) :: a

type MaxBound (Proxy * Bool) :: a

PBounded Ordering (Proxy * Ordering)

Associated Types

type MinBound (Proxy * Ordering) :: a

type MaxBound (Proxy * Ordering) :: a

PBounded () (Proxy * ())

Associated Types

type MinBound (Proxy * ()) :: a

type MaxBound (Proxy * ()) :: a

PBounded (a0, b0) (Proxy * (a0, b0))

Associated Types

type MinBound (Proxy * (a0, b0)) :: a

type MaxBound (Proxy * (a0, b0)) :: a

PBounded (a0, b0, c0) (Proxy * (a0, b0, c0))

Associated Types

type MinBound (Proxy * (a0, b0, c0)) :: a

type MaxBound (Proxy * (a0, b0, c0)) :: a

PBounded (a0, b0, c0, d0) (Proxy * (a0, b0, c0, d0))

Associated Types

type MinBound (Proxy * (a0, b0, c0, d0)) :: a

type MaxBound (Proxy * (a0, b0, c0, d0)) :: a

PBounded (a0, b0, c0, d0, e0) (Proxy * (a0, b0, c0, d0, e0))

Associated Types

type MinBound (Proxy * (a0, b0, c0, d0, e0)) :: a

type MaxBound (Proxy * (a0, b0, c0, d0, e0)) :: a

PBounded (a0, b0, c0, d0, e0, f0) (Proxy * (a0, b0, c0, d0, e0, f0))

Associated Types

type MinBound (Proxy * (a0, b0, c0, d0, e0, f0)) :: a

type MaxBound (Proxy * (a0, b0, c0, d0, e0, f0)) :: a

PBounded (a0, b0, c0, d0, e0, f0, g0) (Proxy * (a0, b0, c0, d0, e0, f0, g0))

Associated Types

type MinBound (Proxy * (a0, b0, c0, d0, e0, f0, g0)) :: a

type MaxBound (Proxy * (a0, b0, c0, d0, e0, f0, g0)) :: 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 a0, SBounded b0) => SBounded (a0, b0)

Methods

sMinBound :: Sing (a0, b0) (MinBoundSym0 (a0, b0))

sMaxBound :: Sing (a0, b0) (MaxBoundSym0 (a0, b0))

(SBounded a0, SBounded b0, SBounded c0) => SBounded (a0, b0, c0)

Methods

sMinBound :: Sing (a0, b0, c0) (MinBoundSym0 (a0, b0, c0))

sMaxBound :: Sing (a0, b0, c0) (MaxBoundSym0 (a0, b0, c0))

(SBounded a0, SBounded b0, SBounded c0, SBounded d0) => SBounded (a0, b0, c0, d0)

Methods

sMinBound :: Sing (a0, b0, c0, d0) (MinBoundSym0 (a0, b0, c0, d0))

sMaxBound :: Sing (a0, b0, c0, d0) (MaxBoundSym0 (a0, b0, c0, d0))

(SBounded a0, SBounded b0, SBounded c0, SBounded d0, SBounded e0) => SBounded (a0, b0, c0, d0, e0)

Methods

sMinBound :: Sing (a0, b0, c0, d0, e0) (MinBoundSym0 (a0, b0, c0, d0, e0))

sMaxBound :: Sing (a0, b0, c0, d0, e0) (MaxBoundSym0 (a0, b0, c0, d0, e0))

(SBounded a0, SBounded b0, SBounded c0, SBounded d0, SBounded e0, SBounded f0) => SBounded (a0, b0, c0, d0, e0, f0)

Methods

sMinBound :: Sing (a0, b0, c0, d0, e0, f0) (MinBoundSym0 (a0, b0, c0, d0, e0, f0))

sMaxBound :: Sing (a0, b0, c0, d0, e0, f0) (MaxBoundSym0 (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)

Methods

sMinBound :: Sing (a0, b0, c0, d0, e0, f0, g0) (MinBoundSym0 (a0, b0, c0, d0, e0, f0, g0))

sMaxBound :: Sing (a0, b0, c0, d0, e0, f0, g0) (MaxBoundSym0 (a0, b0, c0, d0, e0, f0, g0))

class (kproxy ~ Proxy) => PEnum kproxy

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 (Proxy * Bool)

Associated Types

type Succ (Proxy * Bool) (arg :: Proxy * Bool) :: a

type Pred (Proxy * Bool) (arg :: Proxy * Bool) :: a

type ToEnum (Proxy * Bool) (arg :: Nat) :: a

type FromEnum (Proxy * Bool) (arg :: Proxy * Bool) :: Nat

type EnumFromTo (Proxy * Bool) (arg :: Proxy * Bool) (arg :: Proxy * Bool) :: [a]

type EnumFromThenTo (Proxy * Bool) (arg :: Proxy * Bool) (arg :: Proxy * Bool) (arg :: Proxy * Bool) :: [a]

PEnum Ordering (Proxy * Ordering)

Associated Types

type Succ (Proxy * Ordering) (arg :: Proxy * Ordering) :: a

type Pred (Proxy * Ordering) (arg :: Proxy * Ordering) :: a

type ToEnum (Proxy * Ordering) (arg :: Nat) :: a

type FromEnum (Proxy * Ordering) (arg :: Proxy * Ordering) :: Nat

type EnumFromTo (Proxy * Ordering) (arg :: Proxy * Ordering) (arg :: Proxy * Ordering) :: [a]

type EnumFromThenTo (Proxy * Ordering) (arg :: Proxy * Ordering) (arg :: Proxy * Ordering) (arg :: Proxy * Ordering) :: [a]

PEnum Nat (Proxy * Nat)

Associated Types

type Succ (Proxy * Nat) (arg :: Proxy * Nat) :: a

type Pred (Proxy * Nat) (arg :: Proxy * Nat) :: a

type ToEnum (Proxy * Nat) (arg :: Nat) :: a

type FromEnum (Proxy * Nat) (arg :: Proxy * Nat) :: Nat

type EnumFromTo (Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) :: [a]

type EnumFromThenTo (Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) :: [a]

PEnum () (Proxy * ())

Associated Types

type Succ (Proxy * ()) (arg :: Proxy * ()) :: a

type Pred (Proxy * ()) (arg :: Proxy * ()) :: a

type ToEnum (Proxy * ()) (arg :: Nat) :: a

type FromEnum (Proxy * ()) (arg :: Proxy * ()) :: Nat

type EnumFromTo (Proxy * ()) (arg :: Proxy * ()) (arg :: Proxy * ()) :: [a]

type EnumFromThenTo (Proxy * ()) (arg :: Proxy * ()) (arg :: Proxy * ()) (arg :: Proxy * ()) :: [a]

class SEnum a where

Minimal complete definition

sToEnum, sFromEnum

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

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

sEnumFromTo :: forall t t. (Apply (Apply EnumFromToSym0 t) t ~ Apply (Apply EnumFromTo_1627864823Sym0 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_1627864853Sym0 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

Instances

SuppressUnusedWarnings (TyFun a1627864213 a1627864213 -> *) (SuccSym0 a1627864213)

Methods

suppressUnusedWarnings :: Proxy (SuccSym0 a1627864213) t -> ()

type Apply a1627864213 a1627864213 (SuccSym0 a1627864213) l0

type Apply a1627864213 a1627864213 (SuccSym0 a1627864213) l0 = SuccSym1 a1627864213 l0

type SuccSym1 t = Succ t

data PredSym0 l

Instances

SuppressUnusedWarnings (TyFun a1627864213 a1627864213 -> *) (PredSym0 a1627864213)

Methods

suppressUnusedWarnings :: Proxy (PredSym0 a1627864213) t -> ()

type Apply a1627864213 a1627864213 (PredSym0 a1627864213) l0

type Apply a1627864213 a1627864213 (PredSym0 a1627864213) l0 = PredSym1 a1627864213 l0

type PredSym1 t = Pred t

data ToEnumSym0 l

Instances

SuppressUnusedWarnings (TyFun Nat a1627864213 -> *) (ToEnumSym0 a1627864213)

Methods

suppressUnusedWarnings :: Proxy (ToEnumSym0 a1627864213) t -> ()

type Apply Nat k2 (ToEnumSym0 k2) l0

type Apply Nat k2 (ToEnumSym0 k2) l0 = ToEnumSym1 k2 l0

type ToEnumSym1 t = ToEnum t

data FromEnumSym0 l

Instances

SuppressUnusedWarnings (TyFun a1627864213 Nat -> *) (FromEnumSym0 a1627864213)

Methods

suppressUnusedWarnings :: Proxy (FromEnumSym0 a1627864213) t -> ()

type Apply a1627864213 Nat (FromEnumSym0 a1627864213) l0

type Apply a1627864213 Nat (FromEnumSym0 a1627864213) l0 = FromEnumSym1 a1627864213 l0

type FromEnumSym1 t = FromEnum t

data EnumFromToSym0 l

Instances

SuppressUnusedWarnings (TyFun a1627864213 (TyFun a1627864213 [a1627864213] -> Type) -> *) (EnumFromToSym0 a1627864213)

Methods

suppressUnusedWarnings :: Proxy (EnumFromToSym0 a1627864213) t -> ()

type Apply a1627864213 (TyFun a1627864213 [a1627864213] -> Type) (EnumFromToSym0 a1627864213) l0

type Apply a1627864213 (TyFun a1627864213 [a1627864213] -> Type) (EnumFromToSym0 a1627864213) l0 = EnumFromToSym1 a1627864213 l0

data EnumFromToSym1 l l

Instances

SuppressUnusedWarnings (a1627864213 -> TyFun a1627864213 [a1627864213] -> *) (EnumFromToSym1 a1627864213)

Methods

suppressUnusedWarnings :: Proxy (EnumFromToSym1 a1627864213) t -> ()

type Apply a1627864213 [a1627864213] (EnumFromToSym1 a1627864213 l1) l0

type Apply a1627864213 [a1627864213] (EnumFromToSym1 a1627864213 l1) l0 = EnumFromToSym2 a1627864213 l1 l0

type EnumFromToSym2 t t = EnumFromTo t t

data EnumFromThenToSym0 l

Instances

SuppressUnusedWarnings (TyFun a1627864213 (TyFun a1627864213 (TyFun a1627864213 [a1627864213] -> Type) -> Type) -> *) (EnumFromThenToSym0 a1627864213)

Methods

suppressUnusedWarnings :: Proxy (EnumFromThenToSym0 a1627864213) t -> ()

type Apply a1627864213 (TyFun a1627864213 (TyFun a1627864213 [a1627864213] -> Type) -> Type) (EnumFromThenToSym0 a1627864213) l0

type Apply a1627864213 (TyFun a1627864213 (TyFun a1627864213 [a1627864213] -> Type) -> Type) (EnumFromThenToSym0 a1627864213) l0 = EnumFromThenToSym1 a1627864213 l0

data EnumFromThenToSym1 l l

Instances

SuppressUnusedWarnings (a1627864213 -> TyFun a1627864213 (TyFun a1627864213 [a1627864213] -> Type) -> *) (EnumFromThenToSym1 a1627864213)

Methods

suppressUnusedWarnings :: Proxy (EnumFromThenToSym1 a1627864213) t -> ()

type Apply a1627864213 (TyFun a1627864213 [a1627864213] -> Type) (EnumFromThenToSym1 a1627864213 l1) l0

type Apply a1627864213 (TyFun a1627864213 [a1627864213] -> Type) (EnumFromThenToSym1 a1627864213 l1) l0 = EnumFromThenToSym2 a1627864213 l1 l0

data EnumFromThenToSym2 l l l

Instances

SuppressUnusedWarnings (a1627864213 -> a1627864213 -> TyFun a1627864213 [a1627864213] -> *) (EnumFromThenToSym2 a1627864213)

Methods

suppressUnusedWarnings :: Proxy (EnumFromThenToSym2 a1627864213) t -> ()

type Apply a1627864213 [a1627864213] (EnumFromThenToSym2 a1627864213 l1 l2) l0

type Apply a1627864213 [a1627864213] (EnumFromThenToSym2 a1627864213 l1 l2) l0 = EnumFromThenToSym3 a1627864213 l1 l2 l0

type EnumFromThenToSym3 t t t = EnumFromThenTo t t t