singletons-2.5.1: A framework for generating singleton types

Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRyan Scott
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.TH

Contents

Description

This module contains everything you need to derive your own singletons via Template Haskell.

TURN ON -XScopedTypeVariables IN YOUR MODULE IF YOU WANT THIS TO WORK.

Synopsis

Primary Template Haskell generation functions

singletons :: DsMonad q => q [Dec] -> q [Dec] Source #

Make promoted and singleton versions of all declarations given, retaining the original declarations. See https://github.com/goldfirere/singletons/blob/master/README.md for further explanation.

singletonsOnly :: DsMonad q => q [Dec] -> q [Dec] Source #

Make promoted and singleton versions of all declarations given, discarding the original declarations. Note that a singleton based on a datatype needs the original datatype, so this will fail if it sees any datatype declarations. Classes, instances, and functions are all fine.

genSingletons :: DsMonad q => [Name] -> q [Dec] Source #

Generate singleton definitions from a type that is already defined. For example, the singletons package itself uses

$(genSingletons [''Bool, ''Maybe, ''Either, ''[]])

to generate singletons for Prelude types.

promote :: DsMonad q => q [Dec] -> q [Dec] Source #

Promote every declaration given to the type level, retaining the originals.

promoteOnly :: DsMonad q => q [Dec] -> q [Dec] Source #

Promote each declaration, discarding the originals. Note that a promoted datatype uses the same definition as an original datatype, so this will not work with datatypes. Classes, instances, and functions are all fine.

genPromotions :: DsMonad q => [Name] -> q [Dec] Source #

Generate promoted definitions from a type that is already defined. This is generally only useful with classes.

Functions to generate equality instances

promoteEqInstances :: DsMonad q => [Name] -> q [Dec] Source #

Produce instances for (==) (type-level equality) from the given types

promoteEqInstance :: DsMonad q => Name -> q [Dec] Source #

Produce an instance for (==) (type-level equality) from the given type

singEqInstances :: DsMonad q => [Name] -> q [Dec] Source #

Create instances of SEq and type-level (==) for each type in the list

singEqInstance :: DsMonad q => Name -> q [Dec] Source #

Create instance of SEq and type-level (==) for the given type

singEqInstancesOnly :: DsMonad q => [Name] -> q [Dec] Source #

Create instances of SEq (only -- no instance for (==), which SEq generally relies on) for each type in the list

singEqInstanceOnly :: DsMonad q => Name -> q [Dec] Source #

Create instances of SEq (only -- no instance for (==), which SEq generally relies on) for the given type

singDecideInstances :: DsMonad q => [Name] -> q [Dec] Source #

Create instances of SDecide for each type in the list.

singDecideInstance :: DsMonad q => Name -> q [Dec] Source #

Create instance of SDecide for the given type.

Functions to generate Ord instances

promoteOrdInstances :: DsMonad q => [Name] -> q [Dec] Source #

Produce instances for POrd from the given types

promoteOrdInstance :: DsMonad q => Name -> q [Dec] Source #

Produce an instance for POrd from the given type

singOrdInstances :: DsMonad q => [Name] -> q [Dec] Source #

Create instances of SOrd for the given types

singOrdInstance :: DsMonad q => Name -> q [Dec] Source #

Create instance of SOrd for the given type

Functions to generate Bounded instances

promoteBoundedInstances :: DsMonad q => [Name] -> q [Dec] Source #

Produce instances for PBounded from the given types

promoteBoundedInstance :: DsMonad q => Name -> q [Dec] Source #

Produce an instance for PBounded from the given type

singBoundedInstances :: DsMonad q => [Name] -> q [Dec] Source #

Create instances of SBounded for the given types

singBoundedInstance :: DsMonad q => Name -> q [Dec] Source #

Create instance of SBounded for the given type

Functions to generate Enum instances

promoteEnumInstances :: DsMonad q => [Name] -> q [Dec] Source #

Produce instances for PEnum from the given types

promoteEnumInstance :: DsMonad q => Name -> q [Dec] Source #

Produce an instance for PEnum from the given type

singEnumInstances :: DsMonad q => [Name] -> q [Dec] Source #

Create instances of SEnum for the given types

singEnumInstance :: DsMonad q => Name -> q [Dec] Source #

Create instance of SEnum for the given type

Functions to generate Show instances

promoteShowInstances :: DsMonad q => [Name] -> q [Dec] Source #

Produce instances for PShow from the given types

promoteShowInstance :: DsMonad q => Name -> q [Dec] Source #

Produce an instance for PShow from the given type

singShowInstances :: DsMonad q => [Name] -> q [Dec] Source #

Create instances of SShow for the given types

(Not to be confused with showSingInstances.)

singShowInstance :: DsMonad q => Name -> q [Dec] Source #

Create instance of SShow for the given type

(Not to be confused with showShowInstance.)

Utility functions

cases Source #

Arguments

:: DsMonad q 
=> Name

The head of the type of the scrutinee. (Like ''Maybe or ''Bool.)

-> q Exp

The scrutinee, in a Template Haskell quote

-> q Exp

The body, in a Template Haskell quote

-> q Exp 

The function cases generates a case expression where each right-hand side is identical. This may be useful if the type-checker requires knowledge of which constructor is used to satisfy equality or type-class constraints, but where each constructor is treated the same.

sCases Source #

Arguments

:: DsMonad q 
=> Name

The head of the type the scrutinee's type is based on. (Like ''Maybe or ''Bool.)

-> q Exp

The scrutinee, in a Template Haskell quote

-> q Exp

The body, in a Template Haskell quote

-> q Exp 

The function sCases generates a case expression where each right-hand side is identical. This may be useful if the type-checker requires knowledge of which constructor is used to satisfy equality or type-class constraints, but where each constructor is treated the same. For sCases, unlike cases, the scrutinee is a singleton. But make sure to pass in the name of the original datatype, preferring ''Maybe over ''SMaybe.

Basic singleton definitions

data family Sing :: k -> Type Source #

The singleton kind-indexed data family.

Instances
SDecide k => TestCoercion (Sing :: k -> Type) Source # 
Instance details

Defined in Data.Singletons.Decide

Methods

testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) #

SDecide k => TestEquality (Sing :: k -> Type) Source # 
Instance details

Defined in Data.Singletons.Decide

Methods

testEquality :: Sing a -> Sing b -> Maybe (a :~: b) #

Show (SSymbol s) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SSymbol s -> ShowS #

show :: SSymbol s -> String #

showList :: [SSymbol s] -> ShowS #

Show (SNat n) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SNat n -> ShowS #

show :: SNat n -> String #

showList :: [SNat n] -> ShowS #

Eq (Sing a) Source # 
Instance details

Defined in Data.Singletons.TypeRepTYPE

Methods

(==) :: Sing a -> Sing a -> Bool #

(/=) :: Sing a -> Sing a -> Bool #

Ord (Sing a) Source # 
Instance details

Defined in Data.Singletons.TypeRepTYPE

Methods

compare :: Sing a -> Sing a -> Ordering #

(<) :: Sing a -> Sing a -> Bool #

(<=) :: Sing a -> Sing a -> Bool #

(>) :: Sing a -> Sing a -> Bool #

(>=) :: Sing a -> Sing a -> Bool #

max :: Sing a -> Sing a -> Sing a #

min :: Sing a -> Sing a -> Sing a #

Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

(ShowSing a, ShowSing [a]) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

(ShowSing a, ShowSing b) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

Show (Sing a) Source # 
Instance details

Defined in Data.Singletons.TypeRepTYPE

Methods

showsPrec :: Int -> Sing a -> ShowS #

show :: Sing a -> String #

showList :: [Sing a] -> ShowS #

Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

(ShowSing a, ShowSing b) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

(ShowSing a, ShowSing b) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing m => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing (Maybe a) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing (Maybe a) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing (Maybe a) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing Bool => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing Bool => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing a => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

(ShowSing a, ShowSing [a]) => Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

data Sing (a :: Bool) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where
data Sing (a :: Ordering) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where
data Sing (n :: Nat) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where
data Sing (n :: Symbol) Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where
data Sing (a :: ()) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where
data Sing (a :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)
data Sing (a :: All) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where
data Sing (a :: Any) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where
data Sing (a :: PErrorMessage) Source # 
Instance details

Defined in Data.Singletons.TypeError

data Sing (a :: PErrorMessage) where
data Sing (b :: [a]) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where
  • SNil :: forall k (b :: [k]). Sing ([] :: [k])
  • SCons :: forall a (b :: [a]) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n ': n)
data Sing (b :: Maybe a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where
data Sing (a :: TYPE rep) Source #

A choice of singleton for the kind TYPE rep (for some RuntimeRep rep), an instantiation of which is the famous kind Type.

Conceivably, one could generalize this instance to `Sing :: k -> Type` for any kind k, and remove all other Sing instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than TypeReps (for instance, TypeReps are more difficult to pattern match on, and require extra runtime checks).

We cannot produce explicit singleton values for everything in TYPE rep, however, since it is an open kind, so we reach for TypeRep in this one particular case.

Instance details

Defined in Data.Singletons.TypeRepTYPE

data Sing (a :: TYPE rep) = STypeRep (TypeRep a)
data Sing (b :: Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where
data Sing (b :: Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where
data Sing (b :: First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where
data Sing (b :: Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where
data Sing (a :: WrappedMonoid m) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where
data Sing (b :: Option a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where
data Sing (b :: Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where
data Sing (b :: First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where
data Sing (b :: Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where
data Sing (b :: Dual a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where
data Sing (b :: Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where
data Sing (b :: Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where
data Sing (b :: Down a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where
data Sing (b :: NonEmpty a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where
data Sing (c :: Either a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where
data Sing (c :: (a, b)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where
data Sing (c :: Arg a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where
data Sing (f :: k1 ~> k2) Source # 
Instance details

Defined in Data.Singletons.Internal

data Sing (f :: k1 ~> k2) = SLambda {}
data Sing (d :: (a, b, c)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where
data Sing (c :: Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where
data Sing (e :: (a, b, c, d)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where
data Sing (f :: (a, b, c, d, e)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where
data Sing (g :: (a, b, c, d, e, f)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where
data Sing (h :: (a, b, c, d, e, f, g)) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where

Auxiliary definitions

These definitions might be mentioned in code generated by Template Haskell, so they must be in scope.

class PEq a Source #

The promoted analogue of Eq. If you supply no definition for '(==)', then it defaults to a use of DefaultEq.

Associated Types

type (x :: a) == (y :: a) :: Bool infix 4 Source #

type (x :: a) /= (y :: a) :: Bool infix 4 Source #

Instances
PEq Bool Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq Ordering Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq () Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq All Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq Any Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq [a] Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Maybe a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (TYPE rep) Source # 
Instance details

Defined in Data.Singletons.TypeRepTYPE

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (WrappedMonoid m) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Option a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Dual a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Down a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (NonEmpty a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Either a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (a, b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Arg a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (a, b, c) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (a, b, c, d) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (a, b, c, d, e) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (a, b, c, d, e, f) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

PEq (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #

Type-level If. If True a b ==> a; If False a b ==> b

Equations

If True (tru :: k) (fls :: k) = tru 
If False (tru :: k) (fls :: k) = fls 

sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c) Source #

Conditional over singletons

type family (a :: Bool) && (b :: Bool) :: Bool where ... infixr 3 #

Type-level "and"

Equations

False && a = False 
True && a = a 
a && False = False 
a && True = a 
a && a = a 

(%&&) :: Sing a -> Sing b -> Sing (a && b) infixr 3 Source #

Conjunction of singletons

class SEq k where Source #

The singleton analogue of Eq. Unlike the definition for Eq, it is required that instances define a body for '(%==)'. You may also supply a body for '(%/=)'.

Minimal complete definition

(%==)

Methods

(%==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a == b) infix 4 Source #

Boolean equality on singletons

(%/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a /= b) infix 4 Source #

Boolean disequality on singletons

(%/=) :: forall (a :: k) (b :: k). (a /= b) ~ Not (a == b) => Sing a -> Sing b -> Sing (a /= b) infix 4 Source #

Boolean disequality on singletons

Instances
SEq Bool Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #

SEq Ordering Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #

SEq Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #

SEq Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #

SEq () Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #

SEq Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #

SEq Bool => SEq All Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #

SEq Bool => SEq Any Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #

(SEq a, SEq [a]) => SEq [a] Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq a => SEq (Maybe a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq (TYPE rep) Source # 
Instance details

Defined in Data.Singletons.TypeRepTYPE

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #

SEq a => SEq (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq a => SEq (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq a => SEq (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq a => SEq (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq m => SEq (WrappedMonoid m) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #

SEq (Maybe a) => SEq (Option a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq a => SEq (Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq (Maybe a) => SEq (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq (Maybe a) => SEq (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq a => SEq (Dual a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq a => SEq (Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq a => SEq (Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

SEq a => SEq (Down a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

(SEq a, SEq [a]) => SEq (NonEmpty a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source #

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #

(SEq a, SEq b) => SEq (Either a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source #

(%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #

(SEq a, SEq b) => SEq (a, b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source #

(%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #

SEq a => SEq (Arg a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

(%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source #

(%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #

(SEq a, SEq b, SEq c) => SEq (a, b, c) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source #

(%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #

SEq a => SEq (Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

Methods

(%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source #

(%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #

(SEq a, SEq b, SEq c, SEq d) => SEq (a, b, c, d) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source #

(%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #

(SEq a, SEq b, SEq c, SEq d, SEq e) => SEq (a, b, c, d, e) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source #

(%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #

(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) => SEq (a, b, c, d, e, f) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source #

(%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #

(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) => SEq (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) Source #

(%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) Source #

class PEq a => POrd (a :: Type) Source #

Associated Types

type Compare (arg :: a) (arg :: a) :: Ordering Source #

type (arg :: a) < (arg :: a) :: Bool infix 4 Source #

type (arg :: a) <= (arg :: a) :: Bool infix 4 Source #

type (arg :: a) > (arg :: a) :: Bool infix 4 Source #

type (arg :: a) >= (arg :: a) :: Bool infix 4 Source #

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

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

Instances
POrd Bool Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd Ordering Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd () Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd All Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd Any Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd [a] Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Maybe a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (WrappedMonoid m) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Option a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Dual a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Down a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (NonEmpty a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Either a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (a, b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Arg a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (a, b, c) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (a, b, c, d) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (a, b, c, d, e) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (a, b, c, d, e, f) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

class SEq a => SOrd a where Source #

Minimal complete definition

Nothing

Methods

sCompare :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t :: Ordering) Source #

(%<) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t :: Bool) infix 4 Source #

(%<=) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t :: Bool) infix 4 Source #

(%>) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t :: Bool) infix 4 Source #

(%>=) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t :: Bool) infix 4 Source #

sMax :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t :: a) Source #

sMin :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a) Source #

sCompare :: forall (t :: a) (t :: a). (Apply (Apply CompareSym0 t) t :: Ordering) ~ Apply (Apply Compare_6989586621679373674Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t :: Ordering) Source #

(%<) :: forall (t :: a) (t :: a). (Apply (Apply (<@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679373692Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t :: Bool) infix 4 Source #

(%<=) :: forall (t :: a) (t :: a). (Apply (Apply (<=@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679373710Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t :: Bool) infix 4 Source #

(%>) :: forall (t :: a) (t :: a). (Apply (Apply (>@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679373728Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t :: Bool) infix 4 Source #

(%>=) :: forall (t :: a) (t :: a). (Apply (Apply (>=@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679373746Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t :: Bool) infix 4 Source #

sMax :: forall (t :: a) (t :: a). (Apply (Apply MaxSym0 t) t :: a) ~ Apply (Apply Max_6989586621679373764Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t :: a) Source #

sMin :: forall (t :: a) (t :: a). (Apply (Apply MinSym0 t) t :: a) ~ Apply (Apply Min_6989586621679373782Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a) Source #

Instances
SOrd Bool Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd Ordering Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd () Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd Bool => SOrd All Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd Bool => SOrd Any Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

(SOrd a, SOrd [a]) => SOrd [a] Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (Maybe a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd m => SOrd (WrappedMonoid m) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd (Maybe a) => SOrd (Option a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd (Maybe a) => SOrd (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd (Maybe a) => SOrd (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (Dual a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (Down a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

(SOrd a, SOrd [a]) => SOrd (NonEmpty a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

(SOrd a, SOrd b) => SOrd (Either a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

(SOrd a, SOrd b) => SOrd (a, b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (Arg a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

(SOrd a, SOrd b, SOrd c) => SOrd (a, b, c) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

SOrd a => SOrd (Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

(SOrd a, SOrd b, SOrd c, SOrd d) => SOrd (a, b, c, d) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e) => SOrd (a, b, c, d, e) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f) => SOrd (a, b, c, d, e, f) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g) => SOrd (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

type family ThenCmp (a :: Ordering) (a :: Ordering) :: Ordering where ... Source #

Equations

ThenCmp EQ x = x 
ThenCmp LT _ = LTSym0 
ThenCmp GT _ = GTSym0 

sThenCmp :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply ThenCmpSym0 t) t :: Ordering) Source #

class SDecide k where Source #

Members of the SDecide "kind" class support decidable equality. Instances of this class are generated alongside singleton definitions for datatypes that derive an Eq instance.

Methods

(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b) infix 4 Source #

Compute a proof or disproof of equality, given two singletons.

Instances
SDecide Bool Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

SDecide Ordering Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

SDecide Nat Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

SDecide Symbol Source # 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

SDecide () Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

SDecide Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

SDecide Bool => SDecide All Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

SDecide Bool => SDecide Any Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

(SDecide a, SDecide [a]) => SDecide [a] Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide a => SDecide (Maybe a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide (TYPE rep) Source # 
Instance details

Defined in Data.Singletons.TypeRepTYPE

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

SDecide a => SDecide (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide a => SDecide (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide a => SDecide (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide a => SDecide (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide m => SDecide (WrappedMonoid m) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

SDecide (Maybe a) => SDecide (Option a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide a => SDecide (Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide (Maybe a) => SDecide (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide (Maybe a) => SDecide (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide a => SDecide (Dual a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide a => SDecide (Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide a => SDecide (Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

SDecide a => SDecide (Down a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

(SDecide a, SDecide [a]) => SDecide (NonEmpty a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #

(SDecide a, SDecide b) => SDecide (Either a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #

(SDecide a, SDecide b) => SDecide (a, b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #

(SDecide a, SDecide b, SDecide c) => SDecide (a, b, c) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #

SDecide a => SDecide (Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #

(SDecide a, SDecide b, SDecide c, SDecide d) => SDecide (a, b, c, d) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #

(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e) => SDecide (a, b, c, d, e) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #

(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f) => SDecide (a, b, c, d, e, f) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #

(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f, SDecide g) => SDecide (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #

data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type where infix 4 #

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

Refl :: forall k (a :: k) (b :: k). a :~: a 
Instances
TestCoercion ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Coercion

Methods

testCoercion :: (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) #

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

minBound :: a :~: b #

maxBound :: a :~: b #

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b #

pred :: (a :~: b) -> a :~: b #

toEnum :: Int -> a :~: b #

fromEnum :: (a :~: b) -> Int #

enumFrom :: (a :~: b) -> [a :~: b] #

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] #

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] #

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] #

Eq (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool #

(/=) :: (a :~: b) -> (a :~: b) -> Bool #

(a ~ b, Data a) => Data (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Data

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) #

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) #

toConstr :: (a :~: b) -> Constr #

dataTypeOf :: (a :~: b) -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) #

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r #

gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) #

Ord (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering #

(<) :: (a :~: b) -> (a :~: b) -> Bool #

(<=) :: (a :~: b) -> (a :~: b) -> Bool #

(>) :: (a :~: b) -> (a :~: b) -> Bool #

(>=) :: (a :~: b) -> (a :~: b) -> Bool #

max :: (a :~: b) -> (a :~: b) -> a :~: b #

min :: (a :~: b) -> (a :~: b) -> a :~: b #

a ~ b => Read (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b) #

readList :: ReadS [a :~: b] #

readPrec :: ReadPrec (a :~: b) #

readListPrec :: ReadPrec [a :~: b] #

Show (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS #

show :: (a :~: b) -> String #

showList :: [a :~: b] -> ShowS #

data Void #

Uninhabited data type

Since: base-4.8.0.0

Instances
Eq Void

Since: base-4.8.0.0

Instance details

Defined in Data.Void

Methods

(==) :: Void -> Void -> Bool #

(/=) :: Void -> Void -> Bool #

Data Void

Since: base-4.8.0.0

Instance details

Defined in Data.Void

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Void -> c Void #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Void #

toConstr :: Void -> Constr #

dataTypeOf :: Void -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Void) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Void) #

gmapT :: (forall b. Data b => b -> b) -> Void -> Void #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r #

gmapQ :: (forall d. Data d => d -> u) -> Void -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Void -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Void -> m Void #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void #

Ord Void

Since: base-4.8.0.0

Instance details

Defined in Data.Void

Methods

compare :: Void -> Void -> Ordering #

(<) :: Void -> Void -> Bool #

(<=) :: Void -> Void -> Bool #

(>) :: Void -> Void -> Bool #

(>=) :: Void -> Void -> Bool #

max :: Void -> Void -> Void #

min :: Void -> Void -> Void #

Read Void

Reading a Void value is always a parse error, considering Void as a data type with no constructors.

Since: base-4.8.0.0

Instance details

Defined in Data.Void

Show Void

Since: base-4.8.0.0

Instance details

Defined in Data.Void

Methods

showsPrec :: Int -> Void -> ShowS #

show :: Void -> String #

showList :: [Void] -> ShowS #

Ix Void

Since: base-4.8.0.0

Instance details

Defined in Data.Void

Methods

range :: (Void, Void) -> [Void] #

index :: (Void, Void) -> Void -> Int #

unsafeIndex :: (Void, Void) -> Void -> Int

inRange :: (Void, Void) -> Void -> Bool #

rangeSize :: (Void, Void) -> Int #

unsafeRangeSize :: (Void, Void) -> Int

Generic Void 
Instance details

Defined in Data.Void

Associated Types

type Rep Void :: Type -> Type #

Methods

from :: Void -> Rep Void x #

to :: Rep Void x -> Void #

Semigroup Void

Since: base-4.9.0.0

Instance details

Defined in Data.Void

Methods

(<>) :: Void -> Void -> Void #

sconcat :: NonEmpty Void -> Void #

stimes :: Integral b => b -> Void -> Void #

Exception Void

Since: base-4.8.0.0

Instance details

Defined in Data.Void

SingKind Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Associated Types

type Demote Void = (r :: Type) Source #

SDecide Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) Source #

PEq Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool Source #

type x /= y :: Bool Source #

SEq Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) Source #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #

SOrd Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

POrd Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

SSemigroup Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) Source #

sSconcat :: Sing t -> Sing (Apply SconcatSym0 t) Source #

PSemigroup Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type arg <> arg :: a Source #

type Sconcat arg :: a Source #

SShow Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

PShow Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

Associated Types

type ShowsPrec arg arg arg :: Symbol Source #

type Show_ arg :: Symbol Source #

type ShowList arg arg :: Symbol Source #

Show (Sing z) Source # 
Instance details

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

SingI (AbsurdSym0 :: TyFun Void a -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Void

SuppressUnusedWarnings (AbsurdSym0 :: TyFun Void a6989586621679348028 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Void

type Rep Void

Since: base-4.8.0.0

Instance details

Defined in Data.Void

type Rep Void = D1 (MetaData "Void" "Data.Void" "base" False) (V1 :: Type -> Type)
type Demote Void Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)
type Sconcat (arg :: NonEmpty Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sconcat (arg :: NonEmpty Void)
type Show_ (arg :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type Show_ (arg :: Void)
type (a :: Void) == (b :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

type (a :: Void) == (b :: Void)
type (x :: Void) /= (y :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Eq

type (x :: Void) /= (y :: Void) = Not (x == y)
type Compare (a1 :: Void) (a2 :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Compare (a1 :: Void) (a2 :: Void)
type (arg1 :: Void) < (arg2 :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: Void) < (arg2 :: Void)
type (arg1 :: Void) <= (arg2 :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: Void) <= (arg2 :: Void)
type (arg1 :: Void) > (arg2 :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: Void) > (arg2 :: Void)
type (arg1 :: Void) >= (arg2 :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: Void) >= (arg2 :: Void)
type Max (arg1 :: Void) (arg2 :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: Void) (arg2 :: Void)
type Min (arg1 :: Void) (arg2 :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: Void) (arg2 :: Void)
type (a1 :: Void) <> (a2 :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

type (a1 :: Void) <> (a2 :: Void)
type ShowList (arg1 :: [Void]) arg2 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type ShowList (arg1 :: [Void]) arg2
type ShowsPrec a1 (a2 :: Void) a3 Source # 
Instance details

Defined in Data.Singletons.Prelude.Show

type ShowsPrec a1 (a2 :: Void) a3
type Apply (AbsurdSym0 :: TyFun Void k2 -> Type) (a6989586621679348031 :: Void) Source # 
Instance details

Defined in Data.Singletons.Prelude.Void

type Apply (AbsurdSym0 :: TyFun Void k2 -> Type) (a6989586621679348031 :: Void) = (Absurd a6989586621679348031 :: k2)

type Refuted a = a -> Void Source #

Because we can never create a value of type Void, a function that type-checks at a -> Void shows that objects of type a can never exist. Thus, we say that a is Refuted

data Decision a Source #

A Decision about a type a is either a proof of existence or a proof that a cannot exist.

Constructors

Proved a

Witness for a

Disproved (Refuted a)

Proof that no a exists

class PBounded (a :: Type) Source #

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

Instances
PBounded Bool Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded Ordering Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded () Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded All Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded Any Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (WrappedMonoid m) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (Dual a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (a, b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (a, b, c) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (a, b, c, d) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (a, b, c, d, e) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (a, b, c, d, e, f) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

PBounded (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

class SBounded a where Source #

Instances
SBounded Bool Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

SBounded Ordering Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

SBounded () Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

SBounded Bool => SBounded All Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SBounded Bool => SBounded Any Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SBounded a => SBounded (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SBounded a => SBounded (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SBounded a => SBounded (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SBounded a => SBounded (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SBounded m => SBounded (WrappedMonoid m) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SBounded a => SBounded (Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

SBounded a => SBounded (Dual a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SBounded a => SBounded (Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SBounded a => SBounded (Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

(SBounded a, SBounded b) => SBounded (a, b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

(SBounded a, SBounded b, SBounded c) => SBounded (a, b, c) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

SBounded a => SBounded (Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

(SBounded a, SBounded b, SBounded c, SBounded d) => SBounded (a, b, c, d) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e) => SBounded (a, b, c, d, e) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e, SBounded f) => SBounded (a, b, c, d, e, f) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e, SBounded f, SBounded g) => SBounded (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

class PEnum (a :: Type) Source #

Associated Types

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

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

Instances
PEnum Bool Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

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

PEnum Ordering Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

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

PEnum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

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

PEnum () Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

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

PEnum (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

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

PEnum (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

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

PEnum (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

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

PEnum (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

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

PEnum (WrappedMonoid a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

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

PEnum (Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Identity

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

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

PEnum (Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

Associated Types

type Succ arg :: a Source #

type Pred arg :: a Source #

type ToEnum arg :: a Source #

type FromEnum arg :: Nat Source #

type EnumFromTo arg arg :: [a] Source #

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

class SEnum a where Source #

Methods

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

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

Instances
SEnum Bool Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

SEnum Ordering Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

SEnum Nat Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

SEnum () Source # 
Instance details

Defined in Data.Singletons.Prelude.Enum

SEnum a => SEnum (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

SEnum a => SEnum (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

SEnum a => SEnum (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

SEnum a => SEnum (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

SEnum a => SEnum (WrappedMonoid a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup