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 (kproxy ~ Proxy) => PBounded kproxy Source #

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

Instances

PBounded Bool (Proxy * Bool) Source #
Associated Types type MinBound (Proxy * Bool) :: a Source # type MaxBound (Proxy * Bool) :: a Source #
PBounded Ordering (Proxy * Ordering) Source #
Associated Types type MinBound (Proxy * Ordering) :: a Source # type MaxBound (Proxy * Ordering) :: a Source #
PBounded () (Proxy * ()) Source #
Associated Types type MinBound (Proxy * ()) :: a Source # type MaxBound (Proxy * ()) :: a Source #
PBounded (a0, b0) (Proxy * (a0, b0)) Source #
Associated Types type MinBound (Proxy * (a0, b0)) :: a Source # type MaxBound (Proxy * (a0, b0)) :: a Source #
PBounded (a0, b0, c0) (Proxy * (a0, b0, c0)) Source #
Associated Types type MinBound (Proxy * (a0, b0, c0)) :: a Source # type MaxBound (Proxy * (a0, b0, c0)) :: a Source #
PBounded (a0, b0, c0, d0) (Proxy * (a0, b0, c0, d0)) Source #
Associated Types type MinBound (Proxy * (a0, b0, c0, d0)) :: a Source # type MaxBound (Proxy * (a0, b0, c0, d0)) :: a Source #
PBounded (a0, b0, c0, d0, e0) (Proxy * (a0, b0, c0, d0, e0)) Source #
Associated Types type MinBound (Proxy * (a0, b0, c0, d0, e0)) :: a Source # type MaxBound (Proxy * (a0, b0, c0, d0, e0)) :: a Source #
PBounded (a0, b0, c0, d0, e0, f0) (Proxy * (a0, b0, c0, d0, e0, f0)) Source #
Associated Types type MinBound (Proxy * (a0, b0, c0, d0, e0, f0)) :: a Source # type MaxBound (Proxy * (a0, b0, c0, d0, e0, f0)) :: a Source #
PBounded (a0, b0, c0, d0, e0, f0, g0) (Proxy * (a0, b0, c0, d0, e0, f0, g0)) Source #
Associated Types type MinBound (Proxy * (a0, b0, c0, d0, e0, f0, g0)) :: a Source # type MaxBound (Proxy * (a0, b0, c0, d0, e0, f0, g0)) :: a Source #

class SBounded a where Source #

Minimal complete definition

sMinBound, sMaxBound

Methods

sMinBound :: Sing (MinBoundSym0 :: a) Source #

sMaxBound :: Sing (MaxBoundSym0 :: a) Source #

Instances

SBounded Bool Source #
Methods sMinBound :: Sing Bool (MinBoundSym0 Bool) Source # sMaxBound :: Sing Bool (MaxBoundSym0 Bool) Source #
SBounded Ordering Source #
Methods sMinBound :: Sing Ordering (MinBoundSym0 Ordering) Source # sMaxBound :: Sing Ordering (MaxBoundSym0 Ordering) Source #
SBounded () Source #
Methods sMinBound :: Sing () (MinBoundSym0 ()) Source # sMaxBound :: Sing () (MaxBoundSym0 ()) Source #
(SBounded a0, SBounded b0) => SBounded (a0, b0) Source #
Methods sMinBound :: Sing (a0, b0) (MinBoundSym0 (a0, b0)) Source # sMaxBound :: Sing (a0, b0) (MaxBoundSym0 (a0, b0)) Source #
(SBounded a0, SBounded b0, SBounded c0) => SBounded (a0, b0, c0) Source #
Methods sMinBound :: Sing (a0, b0, c0) (MinBoundSym0 (a0, b0, c0)) Source # sMaxBound :: Sing (a0, b0, c0) (MaxBoundSym0 (a0, b0, c0)) Source #
(SBounded a0, SBounded b0, SBounded c0, SBounded d0) => SBounded (a0, b0, c0, d0) Source #
Methods sMinBound :: Sing (a0, b0, c0, d0) (MinBoundSym0 (a0, b0, c0, d0)) Source # sMaxBound :: Sing (a0, b0, c0, d0) (MaxBoundSym0 (a0, b0, c0, d0)) Source #
(SBounded a0, SBounded b0, SBounded c0, SBounded d0, SBounded e0) => SBounded (a0, b0, c0, d0, e0) Source #
Methods sMinBound :: Sing (a0, b0, c0, d0, e0) (MinBoundSym0 (a0, b0, c0, d0, e0)) Source # sMaxBound :: Sing (a0, b0, c0, d0, e0) (MaxBoundSym0 (a0, b0, c0, d0, e0)) Source #
(SBounded a0, SBounded b0, SBounded c0, SBounded d0, SBounded e0, SBounded f0) => SBounded (a0, b0, c0, d0, e0, f0) Source #
Methods sMinBound :: Sing (a0, b0, c0, d0, e0, f0) (MinBoundSym0 (a0, b0, c0, d0, e0, f0)) Source # sMaxBound :: Sing (a0, b0, c0, d0, e0, f0) (MaxBoundSym0 (a0, b0, c0, d0, e0, f0)) Source #
(SBounded a0, SBounded b0, SBounded c0, SBounded d0, SBounded e0, SBounded f0, SBounded g0) => SBounded (a0, b0, c0, d0, e0, f0, g0) Source #
Methods sMinBound :: Sing (a0, b0, c0, d0, e0, f0, g0) (MinBoundSym0 (a0, b0, c0, d0, e0, f0, g0)) Source # sMaxBound :: Sing (a0, b0, c0, d0, e0, f0, g0) (MaxBoundSym0 (a0, b0, c0, d0, e0, f0, g0)) Source #

class (kproxy ~ Proxy) => PEnum kproxy Source #

Associated Types

type Succ (arg :: a) :: a Source #

type Pred (arg :: a) :: a Source #

type ToEnum (arg :: Nat) :: a Source #

type FromEnum (arg :: a) :: Nat Source #

type EnumFromTo (arg :: a) (arg :: a) :: [a] Source #

type EnumFromThenTo (arg :: a) (arg :: a) (arg :: a) :: [a] Source #

Instances

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

class SEnum a where Source #

Minimal complete definition

sToEnum, sFromEnum

Methods

sSucc :: forall t. Sing t -> Sing (Apply SuccSym0 t :: a) Source #

sPred :: forall t. Sing t -> Sing (Apply PredSym0 t :: a) Source #

sToEnum :: forall t. Sing t -> Sing (Apply ToEnumSym0 t :: a) Source #

sFromEnum :: forall t. Sing t -> Sing (Apply FromEnumSym0 t :: Nat) Source #

sEnumFromTo :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t :: [a]) Source #

sEnumFromThenTo :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a]) Source #

sSucc :: forall t. (Apply SuccSym0 t ~ Apply Succ_1627864792Sym0 t) => Sing t -> Sing (Apply SuccSym0 t :: a) Source #

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

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

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

Instances

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

Defunctionalization symbols

type MinBoundSym0 = MinBound Source #

type MaxBoundSym0 = MaxBound Source #

data SuccSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun a1627864213 a1627864213 -> *) (SuccSym0 a1627864213) Source #
Methods suppressUnusedWarnings :: Proxy (SuccSym0 a1627864213) t -> () Source #
type Apply a1627864213 a1627864213 (SuccSym0 a1627864213) l0 Source #
type Apply a1627864213 a1627864213 (SuccSym0 a1627864213) l0 = SuccSym1 a1627864213 l0

type SuccSym1 t = Succ t Source #

data PredSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun a1627864213 a1627864213 -> *) (PredSym0 a1627864213) Source #
Methods suppressUnusedWarnings :: Proxy (PredSym0 a1627864213) t -> () Source #
type Apply a1627864213 a1627864213 (PredSym0 a1627864213) l0 Source #
type Apply a1627864213 a1627864213 (PredSym0 a1627864213) l0 = PredSym1 a1627864213 l0

type PredSym1 t = Pred t Source #

data ToEnumSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun Nat a1627864213 -> *) (ToEnumSym0 a1627864213) Source #
Methods suppressUnusedWarnings :: Proxy (ToEnumSym0 a1627864213) t -> () Source #
type Apply Nat k2 (ToEnumSym0 k2) l0 Source #
type Apply Nat k2 (ToEnumSym0 k2) l0 = ToEnumSym1 k2 l0

type ToEnumSym1 t = ToEnum t Source #

data FromEnumSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun a1627864213 Nat -> *) (FromEnumSym0 a1627864213) Source #
Methods suppressUnusedWarnings :: Proxy (FromEnumSym0 a1627864213) t -> () Source #
type Apply a1627864213 Nat (FromEnumSym0 a1627864213) l0 Source #
type Apply a1627864213 Nat (FromEnumSym0 a1627864213) l0 = FromEnumSym1 a1627864213 l0

type FromEnumSym1 t = FromEnum t Source #

data EnumFromToSym0 l Source #

Instances

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

data EnumFromToSym1 l l Source #

Instances

SuppressUnusedWarnings (a1627864213 -> TyFun a1627864213 [a1627864213] -> *) (EnumFromToSym1 a1627864213) Source #
Methods suppressUnusedWarnings :: Proxy (EnumFromToSym1 a1627864213) t -> () Source #
type Apply a1627864213 [a1627864213] (EnumFromToSym1 a1627864213 l1) l0 Source #
type Apply a1627864213 [a1627864213] (EnumFromToSym1 a1627864213 l1) l0 = EnumFromToSym2 a1627864213 l1 l0

type EnumFromToSym2 t t = EnumFromTo t t Source #

data EnumFromThenToSym0 l Source #

Instances

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

data EnumFromThenToSym1 l l Source #

Instances

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

data EnumFromThenToSym2 l l l Source #

Instances

SuppressUnusedWarnings (a1627864213 -> a1627864213 -> TyFun a1627864213 [a1627864213] -> *) (EnumFromThenToSym2 a1627864213) Source #
Methods suppressUnusedWarnings :: Proxy (EnumFromThenToSym2 a1627864213) t -> () Source #
type Apply a1627864213 [a1627864213] (EnumFromThenToSym2 a1627864213 l1 l2) l0 Source #
type Apply a1627864213 [a1627864213] (EnumFromThenToSym2 a1627864213 l1 l2) l0 = EnumFromThenToSym3 a1627864213 l1 l2 l0

type EnumFromThenToSym3 t t t = EnumFromThenTo t t t Source #