singletons-2.3: A framework for generating singleton types

Copyright(C) 2014 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (rae@cs.brynmawr.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.TypeLits

Contents

Description

Defines and exports singletons useful for the Nat and Symbol kinds.

Synopsis

Documentation

data Nat :: * #

(Kind) This is the kind of type-level natural numbers.

Instances

SNum Nat Source # 
PNum Nat Source # 

Associated Types

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

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

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

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

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

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

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

SEnum Nat Source # 
PEnum Nat Source # 

Associated Types

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

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

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

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

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

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

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$) Source # 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:^$) Source # 
SuppressUnusedWarnings (TyFun Nat Constraint -> *) KnownNatSym0 Source # 
SuppressUnusedWarnings ((TyFun a6989586621679454869 Bool -> Type) -> TyFun [a6989586621679454869] [Nat] -> *) (FindIndicesSym1 a6989586621679454869) Source # 

Methods

suppressUnusedWarnings :: Proxy (FindIndicesSym1 a6989586621679454869) t -> () Source #

SuppressUnusedWarnings ((TyFun a6989586621679454870 Bool -> Type) -> TyFun [a6989586621679454870] (Maybe Nat) -> *) (FindIndexSym1 a6989586621679454870) Source # 

Methods

suppressUnusedWarnings :: Proxy (FindIndexSym1 a6989586621679454870) t -> () Source #

SuppressUnusedWarnings ([a6989586621679454843] -> TyFun Nat a6989586621679454843 -> *) ((:!!$$) a6989586621679454843) Source # 

Methods

suppressUnusedWarnings :: Proxy ((:!!$$) a6989586621679454843) t -> () Source #

SuppressUnusedWarnings (Nat -> TyFun [a6989586621679454860] [a6989586621679454860] -> *) (DropSym1 a6989586621679454860) Source # 

Methods

suppressUnusedWarnings :: Proxy (DropSym1 a6989586621679454860) t -> () Source #

SuppressUnusedWarnings (Nat -> TyFun [a6989586621679454861] [a6989586621679454861] -> *) (TakeSym1 a6989586621679454861) Source # 

Methods

suppressUnusedWarnings :: Proxy (TakeSym1 a6989586621679454861) t -> () Source #

SuppressUnusedWarnings (Nat -> TyFun [a6989586621679454859] ([a6989586621679454859], [a6989586621679454859]) -> *) (SplitAtSym1 a6989586621679454859) Source # 

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym1 a6989586621679454859) t -> () Source #

SuppressUnusedWarnings (Nat -> TyFun a6989586621679454845 [a6989586621679454845] -> *) (ReplicateSym1 a6989586621679454845) Source # 

Methods

suppressUnusedWarnings :: Proxy (ReplicateSym1 a6989586621679454845) t -> () Source #

SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679726400) [a6989586621679726400] -> *) (TakeSym1 a6989586621679726400) Source # 

Methods

suppressUnusedWarnings :: Proxy (TakeSym1 a6989586621679726400) t -> () Source #

SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679726399) [a6989586621679726399] -> *) (DropSym1 a6989586621679726399) Source # 

Methods

suppressUnusedWarnings :: Proxy (DropSym1 a6989586621679726399) t -> () Source #

SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679726398) ([a6989586621679726398], [a6989586621679726398]) -> *) (SplitAtSym1 a6989586621679726398) Source # 

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym1 a6989586621679726398) t -> () Source #

SuppressUnusedWarnings (a6989586621679454871 -> TyFun [a6989586621679454871] [Nat] -> *) (ElemIndicesSym1 a6989586621679454871) Source # 

Methods

suppressUnusedWarnings :: Proxy (ElemIndicesSym1 a6989586621679454871) t -> () Source #

SuppressUnusedWarnings (a6989586621679454872 -> TyFun [a6989586621679454872] (Maybe Nat) -> *) (ElemIndexSym1 a6989586621679454872) Source # 

Methods

suppressUnusedWarnings :: Proxy (ElemIndexSym1 a6989586621679454872) t -> () Source #

SuppressUnusedWarnings (NonEmpty a6989586621679726378 -> TyFun Nat a6989586621679726378 -> *) ((:!!$$) a6989586621679726378) Source # 

Methods

suppressUnusedWarnings :: Proxy ((:!!$$) a6989586621679726378) t -> () Source #

SuppressUnusedWarnings (TyFun (TyFun a6989586621679454869 Bool -> Type) (TyFun [a6989586621679454869] [Nat] -> Type) -> *) (FindIndicesSym0 a6989586621679454869) Source # 

Methods

suppressUnusedWarnings :: Proxy (FindIndicesSym0 a6989586621679454869) t -> () Source #

SuppressUnusedWarnings (TyFun (TyFun a6989586621679454870 Bool -> Type) (TyFun [a6989586621679454870] (Maybe Nat) -> Type) -> *) (FindIndexSym0 a6989586621679454870) Source # 

Methods

suppressUnusedWarnings :: Proxy (FindIndexSym0 a6989586621679454870) t -> () Source #

SuppressUnusedWarnings (TyFun [a6989586621679454843] (TyFun Nat a6989586621679454843 -> Type) -> *) ((:!!$) a6989586621679454843) Source # 

Methods

suppressUnusedWarnings :: Proxy ((:!!$) a6989586621679454843) t -> () Source #

SuppressUnusedWarnings (TyFun [a6989586621679454846] Nat -> *) (LengthSym0 a6989586621679454846) Source # 

Methods

suppressUnusedWarnings :: Proxy (LengthSym0 a6989586621679454846) t -> () Source #

SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679454860] [a6989586621679454860] -> Type) -> *) (DropSym0 a6989586621679454860) Source # 

Methods

suppressUnusedWarnings :: Proxy (DropSym0 a6989586621679454860) t -> () Source #

SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679454861] [a6989586621679454861] -> Type) -> *) (TakeSym0 a6989586621679454861) Source # 

Methods

suppressUnusedWarnings :: Proxy (TakeSym0 a6989586621679454861) t -> () Source #

SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679454859] ([a6989586621679454859], [a6989586621679454859]) -> Type) -> *) (SplitAtSym0 a6989586621679454859) Source # 

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym0 a6989586621679454859) t -> () Source #

SuppressUnusedWarnings (TyFun Nat (TyFun a6989586621679454845 [a6989586621679454845] -> Type) -> *) (ReplicateSym0 a6989586621679454845) Source # 

Methods

suppressUnusedWarnings :: Proxy (ReplicateSym0 a6989586621679454845) t -> () Source #

SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679726400) [a6989586621679726400] -> Type) -> *) (TakeSym0 a6989586621679726400) Source # 

Methods

suppressUnusedWarnings :: Proxy (TakeSym0 a6989586621679726400) t -> () Source #

SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679726399) [a6989586621679726399] -> Type) -> *) (DropSym0 a6989586621679726399) Source # 

Methods

suppressUnusedWarnings :: Proxy (DropSym0 a6989586621679726399) t -> () Source #

SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679726398) ([a6989586621679726398], [a6989586621679726398]) -> Type) -> *) (SplitAtSym0 a6989586621679726398) Source # 

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym0 a6989586621679726398) t -> () Source #

SuppressUnusedWarnings (TyFun Nat a6989586621679407276 -> *) (FromIntegerSym0 a6989586621679407276) Source # 

Methods

suppressUnusedWarnings :: Proxy (FromIntegerSym0 a6989586621679407276) t -> () Source #

SuppressUnusedWarnings (TyFun Nat a6989586621679805857 -> *) (ToEnumSym0 a6989586621679805857) Source # 

Methods

suppressUnusedWarnings :: Proxy (ToEnumSym0 a6989586621679805857) t -> () Source #

SuppressUnusedWarnings (TyFun a6989586621679454871 (TyFun [a6989586621679454871] [Nat] -> Type) -> *) (ElemIndicesSym0 a6989586621679454871) Source # 

Methods

suppressUnusedWarnings :: Proxy (ElemIndicesSym0 a6989586621679454871) t -> () Source #

SuppressUnusedWarnings (TyFun a6989586621679454872 (TyFun [a6989586621679454872] (Maybe Nat) -> Type) -> *) (ElemIndexSym0 a6989586621679454872) Source # 

Methods

suppressUnusedWarnings :: Proxy (ElemIndexSym0 a6989586621679454872) t -> () Source #

SuppressUnusedWarnings (TyFun a6989586621679805857 Nat -> *) (FromEnumSym0 a6989586621679805857) Source # 

Methods

suppressUnusedWarnings :: Proxy (FromEnumSym0 a6989586621679805857) t -> () Source #

SuppressUnusedWarnings (TyFun (NonEmpty a6989586621679726378) (TyFun Nat a6989586621679726378 -> Type) -> *) ((:!!$) a6989586621679726378) Source # 

Methods

suppressUnusedWarnings :: Proxy ((:!!$) a6989586621679726378) t -> () Source #

SuppressUnusedWarnings (TyFun (NonEmpty a6989586621679726431) Nat -> *) (LengthSym0 a6989586621679726431) Source # 

Methods

suppressUnusedWarnings :: Proxy (LengthSym0 a6989586621679726431) t -> () Source #

type Demote Nat Source # 
data Sing Nat Source # 
data Sing Nat where
type Negate Nat a Source # 
type Negate Nat a = Error Symbol Nat "Cannot negate a natural number"
type Abs Nat a Source # 
type Abs Nat a = a
type Signum Nat a Source # 
type Signum Nat a
type FromInteger Nat a Source # 
type FromInteger Nat a = a
type Succ Nat a Source # 
type Succ Nat a
type Pred Nat a Source # 
type Pred Nat a
type ToEnum Nat a Source # 
type ToEnum Nat a
type FromEnum Nat a Source # 
type FromEnum Nat a
type (==) Nat a b 
type (==) Nat a b = EqNat a b
type (:==) Nat a b Source # 
type (:==) Nat a b = (==) Nat a b
type (:/=) Nat x y Source # 
type (:/=) Nat x y = Not ((:==) Nat x y)
type Compare Nat a b Source # 
type Compare Nat a b = CmpNat a b
type (:<) Nat arg1 arg2 Source # 
type (:<) Nat arg1 arg2
type (:<=) Nat arg1 arg2 Source # 
type (:<=) Nat arg1 arg2
type (:>) Nat arg1 arg2 Source # 
type (:>) Nat arg1 arg2
type (:>=) Nat arg1 arg2 Source # 
type (:>=) Nat arg1 arg2
type Max Nat arg1 arg2 Source # 
type Max Nat arg1 arg2
type Min Nat arg1 arg2 Source # 
type Min Nat arg1 arg2
type (:+) Nat a b Source # 
type (:+) Nat a b = (+) a b
type (:-) Nat a b Source # 
type (:-) Nat a b = (-) a b
type (:*) Nat a b Source # 
type (:*) Nat a b = * a b
type EnumFromTo Nat a1 a2 Source # 
type EnumFromTo Nat a1 a2
type Apply Nat Constraint KnownNatSym0 l Source # 
type EnumFromThenTo Nat a1 a2 a3 Source # 
type EnumFromThenTo Nat a1 a2 a3
type Apply Nat Nat ((:^$$) l1) l2 Source # 
type Apply Nat Nat ((:^$$) l1) l2 = (:^) l1 l2
type Apply Nat k2 (FromIntegerSym0 k2) l Source # 
type Apply Nat k2 (FromIntegerSym0 k2) l = FromInteger k2 l
type Apply Nat k2 (ToEnumSym0 k2) l Source # 
type Apply Nat k2 (ToEnumSym0 k2) l = ToEnum k2 l
type Apply a Nat (FromEnumSym0 a) l Source # 
type Apply a Nat (FromEnumSym0 a) l = FromEnum a l
type Apply Nat a ((:!!$$) a l1) l2 Source # 
type Apply Nat a ((:!!$$) a l1) l2 = (:!!) a l1 l2
type Apply Nat a ((:!!$$) a l1) l2 Source # 
type Apply Nat a ((:!!$$) a l1) l2 = (:!!) a l1 l2
type Apply Nat (TyFun Nat Nat -> *) (:^$) l Source # 
type Apply Nat (TyFun Nat Nat -> *) (:^$) l = (:^$$) l
type Apply Nat (TyFun [a6989586621679454860] [a6989586621679454860] -> Type) (DropSym0 a6989586621679454860) l Source # 
type Apply Nat (TyFun [a6989586621679454860] [a6989586621679454860] -> Type) (DropSym0 a6989586621679454860) l = DropSym1 a6989586621679454860 l
type Apply Nat (TyFun [a6989586621679454861] [a6989586621679454861] -> Type) (TakeSym0 a6989586621679454861) l Source # 
type Apply Nat (TyFun [a6989586621679454861] [a6989586621679454861] -> Type) (TakeSym0 a6989586621679454861) l = TakeSym1 a6989586621679454861 l
type Apply Nat (TyFun [a6989586621679454859] ([a6989586621679454859], [a6989586621679454859]) -> Type) (SplitAtSym0 a6989586621679454859) l Source # 
type Apply Nat (TyFun [a6989586621679454859] ([a6989586621679454859], [a6989586621679454859]) -> Type) (SplitAtSym0 a6989586621679454859) l = SplitAtSym1 a6989586621679454859 l
type Apply Nat (TyFun a6989586621679454845 [a6989586621679454845] -> Type) (ReplicateSym0 a6989586621679454845) l Source # 
type Apply Nat (TyFun a6989586621679454845 [a6989586621679454845] -> Type) (ReplicateSym0 a6989586621679454845) l = ReplicateSym1 a6989586621679454845 l
type Apply Nat (TyFun (NonEmpty a6989586621679726400) [a6989586621679726400] -> Type) (TakeSym0 a6989586621679726400) l Source # 
type Apply Nat (TyFun (NonEmpty a6989586621679726400) [a6989586621679726400] -> Type) (TakeSym0 a6989586621679726400) l = TakeSym1 a6989586621679726400 l
type Apply Nat (TyFun (NonEmpty a6989586621679726399) [a6989586621679726399] -> Type) (DropSym0 a6989586621679726399) l Source # 
type Apply Nat (TyFun (NonEmpty a6989586621679726399) [a6989586621679726399] -> Type) (DropSym0 a6989586621679726399) l = DropSym1 a6989586621679726399 l
type Apply Nat (TyFun (NonEmpty a6989586621679726398) ([a6989586621679726398], [a6989586621679726398]) -> Type) (SplitAtSym0 a6989586621679726398) l Source # 
type Apply Nat (TyFun (NonEmpty a6989586621679726398) ([a6989586621679726398], [a6989586621679726398]) -> Type) (SplitAtSym0 a6989586621679726398) l = SplitAtSym1 a6989586621679726398 l
type Apply a6989586621679454871 (TyFun [a6989586621679454871] [Nat] -> Type) (ElemIndicesSym0 a6989586621679454871) l Source # 
type Apply a6989586621679454871 (TyFun [a6989586621679454871] [Nat] -> Type) (ElemIndicesSym0 a6989586621679454871) l = ElemIndicesSym1 a6989586621679454871 l
type Apply a6989586621679454872 (TyFun [a6989586621679454872] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679454872) l Source # 
type Apply a6989586621679454872 (TyFun [a6989586621679454872] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679454872) l = ElemIndexSym1 a6989586621679454872 l
type Apply [a] Nat (LengthSym0 a) l Source # 
type Apply [a] Nat (LengthSym0 a) l = Length a l
type Apply (NonEmpty a) Nat (LengthSym0 a) l Source # 
type Apply (NonEmpty a) Nat (LengthSym0 a) l = Length a l
type Apply [a] [Nat] (FindIndicesSym1 a l1) l2 Source # 
type Apply [a] [Nat] (FindIndicesSym1 a l1) l2 = FindIndices a l1 l2
type Apply [a] [Nat] (ElemIndicesSym1 a l1) l2 Source # 
type Apply [a] [Nat] (ElemIndicesSym1 a l1) l2 = ElemIndices a l1 l2
type Apply [a] (Maybe Nat) (FindIndexSym1 a l1) l2 Source # 
type Apply [a] (Maybe Nat) (FindIndexSym1 a l1) l2 = FindIndex a l1 l2
type Apply [a] (Maybe Nat) (ElemIndexSym1 a l1) l2 Source # 
type Apply [a] (Maybe Nat) (ElemIndexSym1 a l1) l2 = ElemIndex a l1 l2
type Apply [a6989586621679454843] (TyFun Nat a6989586621679454843 -> Type) ((:!!$) a6989586621679454843) l Source # 
type Apply [a6989586621679454843] (TyFun Nat a6989586621679454843 -> Type) ((:!!$) a6989586621679454843) l = (:!!$$) a6989586621679454843 l
type Apply (NonEmpty a6989586621679726378) (TyFun Nat a6989586621679726378 -> Type) ((:!!$) a6989586621679726378) l Source # 
type Apply (NonEmpty a6989586621679726378) (TyFun Nat a6989586621679726378 -> Type) ((:!!$) a6989586621679726378) l = (:!!$$) a6989586621679726378 l
type Apply (TyFun a6989586621679454869 Bool -> Type) (TyFun [a6989586621679454869] [Nat] -> Type) (FindIndicesSym0 a6989586621679454869) l Source # 
type Apply (TyFun a6989586621679454869 Bool -> Type) (TyFun [a6989586621679454869] [Nat] -> Type) (FindIndicesSym0 a6989586621679454869) l = FindIndicesSym1 a6989586621679454869 l
type Apply (TyFun a6989586621679454870 Bool -> Type) (TyFun [a6989586621679454870] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679454870) l Source # 
type Apply (TyFun a6989586621679454870 Bool -> Type) (TyFun [a6989586621679454870] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679454870) l = FindIndexSym1 a6989586621679454870 l

data Symbol :: * #

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

Instances

SingKind Symbol

Since: 4.9.0.0

Associated Types

type DemoteRep Symbol :: *

Methods

fromSing :: Sing Symbol a -> DemoteRep Symbol

KnownSymbol a => SingI Symbol a

Since: 4.9.0.0

Methods

sing :: Sing a a

SuppressUnusedWarnings (TyFun Symbol Constraint -> *) KnownSymbolSym0 Source # 
data Sing Symbol 
data Sing Symbol where
type DemoteRep Symbol 
type DemoteRep Symbol = String
type Demote Symbol Source # 
type Demote Symbol = Text
data Sing Symbol Source # 
data Sing Symbol where
type (==) Symbol a b 
type (==) Symbol a b = EqSymbol a b
type (:==) Symbol a b Source # 
type (:==) Symbol a b = (==) Symbol a b
type (:/=) Symbol x y Source # 
type (:/=) Symbol x y = Not ((:==) Symbol x y)
type Compare Symbol a b Source # 
type Compare Symbol a b = CmpSymbol a b
type (:<) Symbol arg1 arg2 Source # 
type (:<) Symbol arg1 arg2
type (:<=) Symbol arg1 arg2 Source # 
type (:<=) Symbol arg1 arg2
type (:>) Symbol arg1 arg2 Source # 
type (:>) Symbol arg1 arg2
type (:>=) Symbol arg1 arg2 Source # 
type (:>=) Symbol arg1 arg2
type Max Symbol arg1 arg2 Source # 
type Max Symbol arg1 arg2
type Min Symbol arg1 arg2 Source # 
type Min Symbol arg1 arg2
type Apply Symbol Constraint KnownSymbolSym0 l Source # 

data family Sing (a :: k) Source #

The singleton kind-indexed data family.

Instances

data Sing Bool Source # 
data Sing Bool where
data Sing Ordering Source # 
data Sing * Source # 
data Sing * where
data Sing Nat Source # 
data Sing Nat where
data Sing Symbol Source # 
data Sing Symbol where
data Sing () Source # 
data Sing () where
data Sing [a] Source # 
data Sing [a] where
data Sing (Maybe a) Source # 
data Sing (Maybe a) where
data Sing (NonEmpty a) Source # 
data Sing (NonEmpty a) where
data Sing (Either a b) Source # 
data Sing (Either a b) where
data Sing (a, b) Source # 
data Sing (a, b) where
data Sing ((~>) k1 k2) Source # 
data Sing ((~>) k1 k2) = SLambda {}
data Sing (a, b, c) Source # 
data Sing (a, b, c) where
data Sing (a, b, c, d) Source # 
data Sing (a, b, c, d) where
data Sing (a, b, c, d, e) Source # 
data Sing (a, b, c, d, e) where
data Sing (a, b, c, d, e, f) Source # 
data Sing (a, b, c, d, e, f) where
data Sing (a, b, c, d, e, f, g) Source # 
data Sing (a, b, c, d, e, f, g) where

type SNat (x :: Nat) = Sing x Source #

Kind-restricted synonym for Sing for Nats

type SSymbol (x :: Symbol) = Sing x Source #

Kind-restricted synonym for Sing for Symbols

withKnownNat :: Sing n -> (KnownNat n => r) -> r Source #

Given a singleton for Nat, call something requiring a KnownNat instance.

withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r Source #

Given a singleton for Symbol, call something requiring a KnownSymbol instance.

type family Error (str :: k0) :: k Source #

The promotion of error. This version is more poly-kinded for easier use.

data ErrorSym0 (l :: TyFun k06989586621679399311 k6989586621679399313) Source #

Instances

SuppressUnusedWarnings (TyFun k06989586621679399311 k6989586621679399313 -> *) (ErrorSym0 k06989586621679399311 k6989586621679399313) Source # 

Methods

suppressUnusedWarnings :: Proxy (ErrorSym0 k06989586621679399311 k6989586621679399313) t -> () Source #

type Apply k0 k2 (ErrorSym0 k0 k2) l Source # 
type Apply k0 k2 (ErrorSym0 k0 k2) l = Error k0 k2 l

type ErrorSym1 (t :: k06989586621679399311) = Error t Source #

sError :: Sing (str :: Symbol) -> a Source #

The singleton for error

class KnownNat (n :: Nat) #

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

Since: 4.7.0.0

Minimal complete definition

natSing

type KnownNatSym1 (t :: Nat) = KnownNat t Source #

natVal :: KnownNat n => proxy n -> Integer #

Since: 4.7.0.0

class KnownSymbol (n :: Symbol) #

This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

Since: 4.7.0.0

Minimal complete definition

symbolSing

symbolVal :: KnownSymbol n => proxy n -> String #

Since: 4.7.0.0

type (:^) a b = a ^ b infixr 8 Source #

data (l :: Nat) :^$$ l Source #

Instances

type (:^$$$) (t :: Nat) (t :: Nat) = (:^) t t Source #

Orphan instances

Eq Nat Source # 

Methods

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

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

Eq Symbol Source #

This bogus instance is helpful for people who want to define functions over Symbols that will only be used at the type level or as singletons.

Methods

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

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

Num Nat Source #

This bogus Num instance is helpful for people who want to define functions over Nats that will only be used at the type level or as singletons. A correct SNum instance for Nat singletons exists.

Methods

(+) :: Nat -> Nat -> Nat #

(-) :: Nat -> Nat -> Nat #

(*) :: Nat -> Nat -> Nat #

negate :: Nat -> Nat #

abs :: Nat -> Nat #

signum :: Nat -> Nat #

fromInteger :: Integer -> Nat #

Ord Nat Source # 

Methods

compare :: Nat -> Nat -> Ordering #

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

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

(>) :: Nat -> Nat -> Bool #

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

max :: Nat -> Nat -> Nat #

min :: Nat -> Nat -> Nat #

Ord Symbol Source #