halg-core-0.6.0.0: Core types and functions of halg computational algebra suite.

Safe HaskellNone
LanguageHaskell2010

Algebra.Internal

Contents

Synopsis

Documentation

data (a :: k) :~: (b :: k) :: forall k. k -> k -> * 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: 4.7.0.0

Constructors

Refl :: a :~: a 
Instances
Equality ((:=:) :: k -> k -> *) 
Instance details

Methods

symmetry :: (a :=: b) -> b :=: a

Preorder ((:=:) :: k -> k -> *) 
Instance details

Methods

reflexivity :: Sing a -> a :=: a

transitivity :: (a :=: b) -> (b :=: c) -> a :=: c

Semigroupoid ((:~:) :: k -> k -> *) 
Instance details

Methods

o :: (j :~: k1) -> (i :~: j) -> i :~: k1

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

Since: 4.7.0.0

Instance details

Methods

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

NFData2 ((:~:) :: * -> * -> *)

Since: 1.4.3.0

Instance details

Methods

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

NFData1 ((:~:) a)

Since: 1.4.3.0

Instance details

Methods

liftRnf :: (a0 -> ()) -> (a :~: a0) -> () #

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

Since: 4.7.0.0

Instance details

Methods

minBound :: a :~: b #

maxBound :: a :~: b #

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

Since: 4.7.0.0

Instance details

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) 
Instance details

Methods

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

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

Ord (a :~: b) 
Instance details

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: 4.7.0.0

Instance details

Methods

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

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

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

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

Show (a :~: b) 
Instance details

Methods

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

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

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

NFData (a :~: b)

Since: 1.4.3.0

Instance details

Methods

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

withRefl :: (a :~: b) -> ((a ~ b) -> r) -> r #

module Data.Proxy

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

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

data Nat #

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

Instances
PEnum Nat 
Instance details

Associated Types

type Succ arg :: a #

type Pred arg :: a #

type ToEnum arg :: a #

type FromEnum arg :: Nat #

type EnumFromTo arg arg1 :: [a] #

type EnumFromThenTo arg arg1 arg2 :: [a] #

SEnum Nat 
Instance details

Methods

sSucc :: Sing t -> Sing (Apply SuccSym0 t) #

sPred :: Sing t -> Sing (Apply PredSym0 t) #

sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) #

sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) #

sEnumFromTo :: Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2) #

sEnumFromThenTo :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3) #

PNum Nat 
Instance details

Associated Types

type arg + arg1 :: a #

type arg - arg1 :: a #

type arg * arg1 :: a #

type Negate arg :: a #

type Abs arg :: a #

type Signum arg :: a #

type FromInteger arg :: a #

SNum Nat 
Instance details

Methods

(%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) #

(%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) #

(%*) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2) #

sNegate :: Sing t -> Sing (Apply NegateSym0 t) #

sAbs :: Sing t -> Sing (Apply AbsSym0 t) #

sSignum :: Sing t -> Sing (Apply SignumSym0 t) #

sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #

PShow Nat 
Instance details

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol

type Show_ arg :: Symbol

type ShowList arg arg1 :: Symbol

SShow Nat 
Instance details

Methods

sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2)

ShowSing Nat 
Instance details

Methods

showsSingPrec :: Int -> Sing a -> ShowS

KnownNat n => Reifies (n :: Nat) Integer 
Instance details

Methods

reflect :: proxy n -> Integer

(IsMonomialOrder k ord, ones ~ Replicate n 1, SingI ones, (Length ones <= k) ~ True, KnownNat k) => EliminationType k (n :: Nat) (WeightOrder ones ord) Source # 
Instance details
(KnownNat n, KnownNat m, IsMonomialOrder n ord, IsMonomialOrder m ord', k ~ (n + m), KnownNat k) => EliminationType k (n :: Nat) (ProductOrder n m ord ord') Source # 
Instance details
Ord (Monomial n) #

For simplicity, we choose grevlex for the default monomial ordering (for the sake of efficiency).

Instance details

Methods

compare :: Monomial n -> Monomial n -> Ordering #

(<) :: Monomial n -> Monomial n -> Bool #

(<=) :: Monomial n -> Monomial n -> Bool #

(>) :: Monomial n -> Monomial n -> Bool #

(>=) :: Monomial n -> Monomial n -> Bool #

max :: Monomial n -> Monomial n -> Monomial n #

min :: Monomial n -> Monomial n -> Monomial n #

KnownNat n => Unital (Monomial n) # 
Instance details

Methods

one :: Monomial n #

pow :: Monomial n -> Natural -> Monomial n #

productWith :: Foldable f => (a -> Monomial n) -> f a -> Monomial n #

Multiplicative (Monomial n) # 
Instance details

Methods

(*) :: Monomial n -> Monomial n -> Monomial n #

pow1p :: Monomial n -> Natural -> Monomial n #

productWith1 :: Foldable1 f => (a -> Monomial n) -> f a -> Monomial n #

(SingI m, SingI n, n ~ (m + 1)) => Bounded (Ordinal n) 
Instance details

Methods

minBound :: Ordinal n #

maxBound :: Ordinal n #

SuppressUnusedWarnings ShowsPrec_6989586621679944083Sym2 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944128Sym2 
Instance details
SuppressUnusedWarnings EfdtNatDnSym2 
Instance details
SuppressUnusedWarnings EfdtNatSym2 
Instance details
SuppressUnusedWarnings EfdtNatUpSym2 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679928013Sym2 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679943886Sym2 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944174Sym2 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944083Sym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944128Sym1 
Instance details
SuppressUnusedWarnings EfdtNatDnSym1 
Instance details
SuppressUnusedWarnings EfdtNatSym1 
Instance details
SuppressUnusedWarnings EfdtNatUpSym1 
Instance details
SuppressUnusedWarnings EftNatSym1 
Instance details
SuppressUnusedWarnings (^@#@$$) 
Instance details
SuppressUnusedWarnings DivSym1 
Instance details
SuppressUnusedWarnings ModSym1 
Instance details
SuppressUnusedWarnings QuotSym1 
Instance details
SuppressUnusedWarnings RemSym1 
Instance details
SuppressUnusedWarnings DivModSym1 
Instance details
SuppressUnusedWarnings QuotRemSym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679928013Sym1 
Instance details
SuppressUnusedWarnings ShowsNatSym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679943886Sym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944174Sym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679059182Sym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679059182Sym2 
Instance details
SuppressUnusedWarnings FromEnum_6989586621680088518Sym0 
Instance details
SuppressUnusedWarnings FromEnum_6989586621680088550Sym0 
Instance details
SuppressUnusedWarnings ToEnum_6989586621680088508Sym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944083Sym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944128Sym0 
Instance details
SuppressUnusedWarnings EfdtNatDnSym0 
Instance details
SuppressUnusedWarnings EfdtNatSym0 
Instance details
SuppressUnusedWarnings EfdtNatUpSym0 
Instance details
SuppressUnusedWarnings EftNatSym0 
Instance details
SuppressUnusedWarnings (^@#@$) 
Instance details
SuppressUnusedWarnings DivSym0 
Instance details
SuppressUnusedWarnings ModSym0 
Instance details
SuppressUnusedWarnings QuotSym0 
Instance details
SuppressUnusedWarnings RemSym0 
Instance details
SuppressUnusedWarnings DivModSym0 
Instance details
SuppressUnusedWarnings QuotRemSym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679928013Sym0 
Instance details
SuppressUnusedWarnings ShowsNatSym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679943886Sym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944174Sym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679059182Sym0 
Instance details
SuppressUnusedWarnings ToEnum_6989586621680088540Sym0 
Instance details
SuppressUnusedWarnings KnownNatSym0 
Instance details
SuppressUnusedWarnings Log2Sym0 
Instance details
SuppressUnusedWarnings ToEnum_6989586621680088565Sym0 
Instance details
SuppressUnusedWarnings FromInteger_6989586621679099356Sym0 
Instance details
SuppressUnusedWarnings ToEnum_6989586621679102522Sym0 
Instance details
SuppressUnusedWarnings FromEnum_6989586621680088575Sym0 
Instance details
SuppressUnusedWarnings FromEnum_6989586621679102533Sym0 
Instance details
SuppressUnusedWarnings (FindIndicesSym1 :: (TyFun a6989586621679715492 Bool -> Type) -> TyFun [a6989586621679715492] [Nat] -> *) 
Instance details
SuppressUnusedWarnings (FindIndexSym1 :: (TyFun a6989586621679715493 Bool -> Type) -> TyFun [a6989586621679715493] (Maybe Nat) -> *) 
Instance details
SuppressUnusedWarnings ((!!@#@$$) :: [a6989586621679715466] -> TyFun Nat a6989586621679715466 -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927975Sym2 :: Nat -> [a6989586621679925850] -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943933Sym2 :: Nat -> Maybe a3530822107858468865 -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927904Sym2 :: Nat -> a6989586621679925832 -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrecSym2 :: Nat -> a6989586621679925832 -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679944039Sym2 :: Nat -> NonEmpty a6989586621679060556 -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927975Sym1 :: Nat -> TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (TakeSym1 :: Nat -> TyFun [a6989586621679715484] [a6989586621679715484] -> *) 
Instance details
SuppressUnusedWarnings (SplitAtSym1 :: Nat -> TyFun [a6989586621679715482] ([a6989586621679715482], [a6989586621679715482]) -> *) 
Instance details
SuppressUnusedWarnings (DropSym1 :: Nat -> TyFun [a6989586621679715483] [a6989586621679715483] -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943933Sym1 :: Nat -> TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927904Sym1 :: Nat -> TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrecSym1 :: Nat -> TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ReplicateSym1 :: Nat -> TyFun a6989586621679715468 [a6989586621679715468] -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679944039Sym1 :: Nat -> TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ElemIndicesSym1 :: a6989586621679715494 -> TyFun [a6989586621679715494] [Nat] -> *) 
Instance details
SuppressUnusedWarnings (ElemIndexSym1 :: a6989586621679715495 -> TyFun [a6989586621679715495] (Maybe Nat) -> *) 
Instance details
SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (TyFun a6989586621679715492 Bool -> Type) (TyFun [a6989586621679715492] [Nat] -> Type) -> *) 
Instance details
SuppressUnusedWarnings (FindIndexSym0 :: TyFun (TyFun a6989586621679715493 Bool -> Type) (TyFun [a6989586621679715493] (Maybe Nat) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (LengthSym0 :: TyFun [a6989586621679715469] Nat -> *) 
Instance details
SuppressUnusedWarnings ((!!@#@$) :: TyFun [a6989586621679715466] (TyFun Nat a6989586621679715466 -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927975Sym0 :: TyFun Nat (TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat (TyFun [a6989586621679715484] [a6989586621679715484] -> Type) -> *) 
Instance details
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat (TyFun [a6989586621679715482] ([a6989586621679715482], [a6989586621679715482]) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (DropSym0 :: TyFun Nat (TyFun [a6989586621679715483] [a6989586621679715483] -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943933Sym0 :: TyFun Nat (TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927904Sym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ReplicateSym0 :: TyFun Nat (TyFun a6989586621679715468 [a6989586621679715468] -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679944039Sym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679686791 -> *) 
Instance details
SuppressUnusedWarnings (ToEnum_6989586621680070067Sym0 :: TyFun Nat a6989586621680069317 -> *) 
Instance details
SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a6989586621680069317 -> *) 
Instance details
SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a6989586621679715494 (TyFun [a6989586621679715494] [Nat] -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a6989586621679715495 (TyFun [a6989586621679715495] (Maybe Nat) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (FromEnum_6989586621680070078Sym0 :: TyFun a6989586621680069317 Nat -> *) 
Instance details
SuppressUnusedWarnings (FromEnumSym0 :: TyFun a6989586621680069317 Nat -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943989Sym2 :: Nat -> Either a6989586621679082540 b6989586621679082541 -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928048Sym2 :: Nat -> (a6989586621679925854, b6989586621679925855) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943989Sym1 :: Nat -> TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928048Sym1 :: Nat -> TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943989Sym0 :: TyFun Nat (TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928048Sym0 :: TyFun Nat (TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928084Sym2 :: Nat -> (a6989586621679925859, b6989586621679925860, c6989586621679925861) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928084Sym1 :: Nat -> TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679725985BuildListSym3 :: k1 -> k2 -> Nat -> TyFun [b6989586621679715945] [Nat] -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679725985BuildListSym2 :: k1 -> k2 -> TyFun Nat (TyFun [b6989586621679715945] [Nat] -> Type) -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679725985BuildListSym1 :: k1 -> TyFun k2 (TyFun Nat (TyFun [b6989586621679715945] [Nat] -> Type) -> *) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928084Sym0 :: TyFun Nat (TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679725985BuildListSym0 :: TyFun k1 (TyFun k2 (TyFun Nat (TyFun [b6989586621679715945] [Nat] -> Type) -> *) -> *) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928121Sym2 :: Nat -> (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928121Sym1 :: Nat -> TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928121Sym0 :: TyFun Nat (TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928159Sym2 :: Nat -> (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928159Sym1 :: Nat -> TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928159Sym0 :: TyFun Nat (TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928198Sym2 :: Nat -> (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928198Sym1 :: Nat -> TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928198Sym0 :: TyFun Nat (TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928238Sym2 :: Nat -> (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928238Sym1 :: Nat -> TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928238Sym0 :: TyFun Nat (TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
data Sing (n :: Nat) 
Instance details
data Sing (n :: Nat) where
type Demote Nat 
Instance details
type FromEnum (a :: Nat) 
Instance details
type FromEnum (a :: Nat) = Apply (FromEnum_6989586621680070078Sym0 :: TyFun Nat Nat -> *) a
type ToEnum a 
Instance details
type ToEnum a = Apply (ToEnum_6989586621680070067Sym0 :: TyFun Nat Nat -> *) a
type Abs (a :: Nat) 
Instance details
type Abs (a :: Nat) = a
type FromInteger a 
Instance details
type FromInteger a = a
type Negate (a :: Nat) 
Instance details
type Negate (a :: Nat) = (Error "Cannot negate a natural number" :: Nat)
type Signum (a :: Nat) 
Instance details
type Signum (a :: Nat) = SignumNat a
type Show_ (arg :: Nat) 
Instance details
type Show_ (arg :: Nat) = Apply (Show__6989586621679927924Sym0 :: TyFun Nat Symbol -> *) arg
type Pred (a :: Nat) 
Instance details
type Pred (a :: Nat) = Apply (Pred_6989586621680070056Sym0 :: TyFun Nat Nat -> *) a
type Succ (a :: Nat) 
Instance details
type Succ (a :: Nat) = Apply (Succ_6989586621680070045Sym0 :: TyFun Nat Nat -> *) a
type EnumFromTo (a1 :: Nat) (a2 :: Nat) 
Instance details
type EnumFromTo (a1 :: Nat) (a2 :: Nat) = Apply (Apply (EnumFromTo_6989586621680070100Sym0 :: TyFun Nat (TyFun Nat [Nat] -> Type) -> *) a1) a2
type (x :: Nat) /= (y :: Nat) 
Instance details
type (x :: Nat) /= (y :: Nat) = Not (x == y)
type (a :: Nat) == (b :: Nat) 
Instance details
type (a :: Nat) == (b :: Nat) = a == b
type (a :: Nat) * (b :: Nat) 
Instance details
type (a :: Nat) * (b :: Nat) = a * b
type (a :: Nat) + (b :: Nat) 
Instance details
type (a :: Nat) + (b :: Nat) = a + b
type (a :: Nat) - (b :: Nat) 
Instance details
type (a :: Nat) - (b :: Nat) = a - b
type (arg1 :: Nat) < (arg2 :: Nat) 
Instance details
type (arg1 :: Nat) < (arg2 :: Nat) = Apply (Apply (TFHelper_6989586621679569644Sym0 :: TyFun Nat (TyFun Nat Bool -> Type) -> *) arg1) arg2
type (arg1 :: Nat) <= (arg2 :: Nat) 
Instance details
type (arg1 :: Nat) <= (arg2 :: Nat) = Apply (Apply (TFHelper_6989586621679569677Sym0 :: TyFun Nat (TyFun Nat Bool -> Type) -> *) arg1) arg2
type (arg1 :: Nat) > (arg2 :: Nat) 
Instance details
type (arg1 :: Nat) > (arg2 :: Nat) = Apply (Apply (TFHelper_6989586621679569710Sym0 :: TyFun Nat (TyFun Nat Bool -> Type) -> *) arg1) arg2
type (arg1 :: Nat) >= (arg2 :: Nat) 
Instance details
type (arg1 :: Nat) >= (arg2 :: Nat) = Apply (Apply (TFHelper_6989586621679569743Sym0 :: TyFun Nat (TyFun Nat Bool -> Type) -> *) arg1) arg2
type Compare (a :: Nat) (b :: Nat) 
Instance details
type Compare (a :: Nat) (b :: Nat) = CmpNat a b
type Max (arg1 :: Nat) (arg2 :: Nat) 
Instance details
type Max (arg1 :: Nat) (arg2 :: Nat) = Apply (Apply (Max_6989586621679569776Sym0 :: TyFun Nat (TyFun Nat Nat -> Type) -> *) arg1) arg2
type Min (arg1 :: Nat) (arg2 :: Nat) 
Instance details
type Min (arg1 :: Nat) (arg2 :: Nat) = Apply (Apply (Min_6989586621679569809Sym0 :: TyFun Nat (TyFun Nat Nat -> Type) -> *) arg1) arg2
type ShowList (arg1 :: [Nat]) arg2 
Instance details
type ShowList (arg1 :: [Nat]) arg2 = Apply (Apply (ShowList_6989586621679927942Sym0 :: TyFun [Nat] (TyFun Symbol Symbol -> Type) -> *) arg1) arg2
type Apply FromEnum_6989586621680088518Sym0 (l :: Bool) 
Instance details
type Apply FromEnum_6989586621680088518Sym0 (l :: Bool) = FromEnum_6989586621680088518 l
type Apply FromEnum_6989586621680088550Sym0 (l :: Ordering) 
Instance details
type Apply FromEnum_6989586621680088550Sym0 (l :: Ordering) = FromEnum_6989586621680088550 l
type Apply ToEnum_6989586621680088508Sym0 (l :: Nat) 
Instance details
type Apply ToEnum_6989586621680088508Sym0 (l :: Nat) = ToEnum_6989586621680088508 l
type Apply ToEnum_6989586621680088540Sym0 (l :: Nat) 
Instance details
type Apply ToEnum_6989586621680088540Sym0 (l :: Nat) = ToEnum_6989586621680088540 l
type Apply KnownNatSym0 (l :: Nat) 
Instance details
type Apply KnownNatSym0 (l :: Nat) = KnownNat l
type Apply Log2Sym0 (l :: Nat) 
Instance details
type Apply Log2Sym0 (l :: Nat) = Log2 l
type Apply ToEnum_6989586621680088565Sym0 (l :: Nat) 
Instance details
type Apply ToEnum_6989586621680088565Sym0 (l :: Nat) = ToEnum_6989586621680088565 l
type Apply FromInteger_6989586621679099356Sym0 (l :: Nat) 
Instance details
type Apply FromInteger_6989586621679099356Sym0 (l :: Nat) = FromInteger_6989586621679099356 l
type Apply ToEnum_6989586621679102522Sym0 (l :: Nat) 
Instance details
type Apply ToEnum_6989586621679102522Sym0 (l :: Nat) = ToEnum_6989586621679102522 l
type Apply FromEnum_6989586621680088575Sym0 (l :: ()) 
Instance details
type Apply FromEnum_6989586621680088575Sym0 (l :: ()) = FromEnum_6989586621680088575 l
type Apply FromEnum_6989586621679102533Sym0 (l :: Nat) 
Instance details
type Apply FromEnum_6989586621679102533Sym0 (l :: Nat) = FromEnum_6989586621679102533 l
type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat) 
Instance details
type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat) = Apply (Apply (Apply (EnumFromThenTo_6989586621680070136Sym0 :: TyFun Nat (TyFun Nat (TyFun Nat [Nat] -> Type) -> Type) -> *) a1) a2) a3
type ShowsPrec _ (n :: Nat) x 
Instance details
type ShowsPrec _ (n :: Nat) x = ShowsNat n x
type Apply ((^@#@$$) l1 :: TyFun Nat Nat -> *) (l2 :: Nat) 
Instance details
type Apply ((^@#@$$) l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = l1 ^ l2
type Apply (DivSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) 
Instance details
type Apply (DivSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Div l1 l2
type Apply (ModSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) 
Instance details
type Apply (ModSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Mod l1 l2
type Apply (QuotSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) 
Instance details
type Apply (QuotSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Quot l1 l2
type Apply (RemSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) 
Instance details
type Apply (RemSym1 l1 :: TyFun Nat Nat -> *) (l2 :: Nat) = Rem l1 l2
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) 
Instance details
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) = (FromInteger l :: k2)
type Apply (ToEnumSym0 :: TyFun Nat k2 -> *) (l :: Nat) 
Instance details
type Apply (ToEnumSym0 :: TyFun Nat k2 -> *) (l :: Nat) = (ToEnum l :: k2)
type Apply (ToEnum_6989586621680070067Sym0 :: TyFun Nat k2 -> *) (l :: Nat) 
Instance details
type Apply (ToEnum_6989586621680070067Sym0 :: TyFun Nat k2 -> *) (l :: Nat) = (ToEnum_6989586621680070067 l :: k2)
type Apply (FromEnumSym0 :: TyFun a Nat -> *) (l :: a) 
Instance details
type Apply (FromEnumSym0 :: TyFun a Nat -> *) (l :: a) = FromEnum l
type Apply (FromEnum_6989586621680070078Sym0 :: TyFun a Nat -> *) (l :: a) 
Instance details
type Apply (FromEnum_6989586621680070078Sym0 :: TyFun a Nat -> *) (l :: a) = FromEnum_6989586621680070078 l
type Apply ((!!@#@$$) l1 :: TyFun Nat a -> *) (l2 :: Nat) 
Instance details
type Apply ((!!@#@$$) l1 :: TyFun Nat a -> *) (l2 :: Nat) = l1 !! l2
type Apply (EftNatSym1 l1 :: TyFun Nat [Nat] -> *) (l2 :: Nat) 
Instance details
type Apply (EftNatSym1 l1 :: TyFun Nat [Nat] -> *) (l2 :: Nat) = EftNat l1 l2
type Apply (EfdtNatDnSym2 l1 l2 :: TyFun Nat [Nat] -> *) (l3 :: Nat) 
Instance details
type Apply (EfdtNatDnSym2 l1 l2 :: TyFun Nat [Nat] -> *) (l3 :: Nat) = EfdtNatDn l1 l2 l3
type Apply (EfdtNatSym2 l1 l2 :: TyFun Nat [Nat] -> *) (l3 :: Nat) 
Instance details
type Apply (EfdtNatSym2 l1 l2 :: TyFun Nat [Nat] -> *) (l3 :: Nat) = EfdtNat l1 l2 l3
type Apply (EfdtNatUpSym2 l1 l2 :: TyFun Nat [Nat] -> *) (l3 :: Nat) 
Instance details
type Apply (EfdtNatUpSym2 l1 l2 :: TyFun Nat [Nat] -> *) (l3 :: Nat) = EfdtNatUp l1 l2 l3
type Apply ShowsPrec_6989586621679944083Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679944083Sym0 (l :: Nat) = ShowsPrec_6989586621679944083Sym1 l
type Apply ShowsPrec_6989586621679944128Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679944128Sym0 (l :: Nat) = ShowsPrec_6989586621679944128Sym1 l
type Apply EfdtNatDnSym0 (l :: Nat) 
Instance details
type Apply EfdtNatDnSym0 (l :: Nat) = EfdtNatDnSym1 l
type Apply EfdtNatSym0 (l :: Nat) 
Instance details
type Apply EfdtNatSym0 (l :: Nat) = EfdtNatSym1 l
type Apply EfdtNatUpSym0 (l :: Nat) 
Instance details
type Apply EfdtNatUpSym0 (l :: Nat) = EfdtNatUpSym1 l
type Apply EftNatSym0 (l :: Nat) 
Instance details
type Apply EftNatSym0 (l :: Nat) = EftNatSym1 l
type Apply (^@#@$) (l :: Nat) 
Instance details
type Apply (^@#@$) (l :: Nat) = (^@#@$$) l
type Apply DivSym0 (l :: Nat) 
Instance details
type Apply DivSym0 (l :: Nat) = DivSym1 l
type Apply ModSym0 (l :: Nat) 
Instance details
type Apply ModSym0 (l :: Nat) = ModSym1 l
type Apply QuotSym0 (l :: Nat) 
Instance details
type Apply QuotSym0 (l :: Nat) = QuotSym1 l
type Apply RemSym0 (l :: Nat) 
Instance details
type Apply RemSym0 (l :: Nat) = RemSym1 l
type Apply DivModSym0 (l :: Nat) 
Instance details
type Apply DivModSym0 (l :: Nat) = DivModSym1 l
type Apply QuotRemSym0 (l :: Nat) 
Instance details
type Apply QuotRemSym0 (l :: Nat) = QuotRemSym1 l
type Apply ShowsPrec_6989586621679928013Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679928013Sym0 (l :: Nat) = ShowsPrec_6989586621679928013Sym1 l
type Apply ShowsNatSym0 (l :: Nat) 
Instance details
type Apply ShowsNatSym0 (l :: Nat) = ShowsNatSym1 l
type Apply ShowsPrec_6989586621679943886Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679943886Sym0 (l :: Nat) = ShowsPrec_6989586621679943886Sym1 l
type Apply ShowsPrec_6989586621679944174Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679944174Sym0 (l :: Nat) = ShowsPrec_6989586621679944174Sym1 l
type Apply ShowsPrec_6989586621679059182Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679059182Sym0 (l :: Nat) = ShowsPrec_6989586621679059182Sym1 l
type Apply (ShowsPrec_6989586621679927975Sym0 :: TyFun Nat (TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679927975Sym0 :: TyFun Nat (TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679927975Sym1 l :: TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> *)
type Apply (DropSym0 :: TyFun Nat (TyFun [a6989586621679715483] [a6989586621679715483] -> Type) -> *) (l :: Nat) 
Instance details
type Apply (DropSym0 :: TyFun Nat (TyFun [a6989586621679715483] [a6989586621679715483] -> Type) -> *) (l :: Nat) = (DropSym1 l :: TyFun [a6989586621679715483] [a6989586621679715483] -> *)
type Apply (TakeSym0 :: TyFun Nat (TyFun [a6989586621679715484] [a6989586621679715484] -> Type) -> *) (l :: Nat) 
Instance details
type Apply (TakeSym0 :: TyFun Nat (TyFun [a6989586621679715484] [a6989586621679715484] -> Type) -> *) (l :: Nat) = (TakeSym1 l :: TyFun [a6989586621679715484] [a6989586621679715484] -> *)
type Apply (SplitAtSym0 :: TyFun Nat (TyFun [a6989586621679715482] ([a6989586621679715482], [a6989586621679715482]) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (SplitAtSym0 :: TyFun Nat (TyFun [a6989586621679715482] ([a6989586621679715482], [a6989586621679715482]) -> Type) -> *) (l :: Nat) = (SplitAtSym1 l :: TyFun [a6989586621679715482] ([a6989586621679715482], [a6989586621679715482]) -> *)
type Apply (ShowsPrec_6989586621679943933Sym0 :: TyFun Nat (TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679943933Sym0 :: TyFun Nat (TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679943933Sym1 l :: TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> *)
type Apply (EfdtNatDnSym1 l1 :: TyFun Nat (TyFun Nat [Nat] -> Type) -> *) (l2 :: Nat) 
Instance details
type Apply (EfdtNatDnSym1 l1 :: TyFun Nat (TyFun Nat [Nat] -> Type) -> *) (l2 :: Nat) = EfdtNatDnSym2 l1 l2
type Apply (EfdtNatSym1 l1 :: TyFun Nat (TyFun Nat [Nat] -> Type) -> *) (l2 :: Nat) 
Instance details
type Apply (EfdtNatSym1 l1 :: TyFun Nat (TyFun Nat [Nat] -> Type) -> *) (l2 :: Nat) = EfdtNatSym2 l1 l2
type Apply (EfdtNatUpSym1 l1 :: TyFun Nat (TyFun Nat [Nat] -> Type) -> *) (l2 :: Nat) 
Instance details
type Apply (EfdtNatUpSym1 l1 :: TyFun Nat (TyFun Nat [Nat] -> Type) -> *) (l2 :: Nat) = EfdtNatUpSym2 l1 l2
type Apply (ReplicateSym0 :: TyFun Nat (TyFun a6989586621679715468 [a6989586621679715468] -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ReplicateSym0 :: TyFun Nat (TyFun a6989586621679715468 [a6989586621679715468] -> Type) -> *) (l :: Nat) = (ReplicateSym1 l :: TyFun a6989586621679715468 [a6989586621679715468] -> *)
type Apply (ShowsPrec_6989586621679927904Sym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679927904Sym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679927904Sym1 l :: TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrecSym1 l :: TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrec_6989586621679944039Sym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679944039Sym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679944039Sym1 l :: TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> *)
type Apply (DivModSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) 
Instance details
type Apply (DivModSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) = DivMod l1 l2
type Apply (QuotRemSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) 
Instance details
type Apply (QuotRemSym1 l1 :: TyFun Nat (Nat, Nat) -> *) (l2 :: Nat) = QuotRem l1 l2
type Apply (ElemIndicesSym0 :: TyFun a6989586621679715494 (TyFun [a6989586621679715494] [Nat] -> Type) -> *) (l :: a6989586621679715494) 
Instance details
type Apply (ElemIndicesSym0 :: TyFun a6989586621679715494 (TyFun [a6989586621679715494] [Nat] -> Type) -> *) (l :: a6989586621679715494) = ElemIndicesSym1 l
type Apply (ElemIndexSym0 :: TyFun a6989586621679715495 (TyFun [a6989586621679715495] (Maybe Nat) -> Type) -> *) (l :: a6989586621679715495) 
Instance details
type Apply (ElemIndexSym0 :: TyFun a6989586621679715495 (TyFun [a6989586621679715495] (Maybe Nat) -> Type) -> *) (l :: a6989586621679715495) = ElemIndexSym1 l
type Apply (ShowsPrec_6989586621679943989Sym0 :: TyFun Nat (TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679943989Sym0 :: TyFun Nat (TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679943989Sym1 l :: TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrec_6989586621679928048Sym0 :: TyFun Nat (TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928048Sym0 :: TyFun Nat (TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928048Sym1 l :: TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrec_6989586621679928084Sym0 :: TyFun Nat (TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928084Sym0 :: TyFun Nat (TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928084Sym1 l :: TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> *)
type Apply (Let6989586621679725985BuildListSym0 :: TyFun k1 (TyFun k2 (TyFun Nat (TyFun [b6989586621679715945] [Nat] -> Type) -> *) -> *) -> *) (l :: k1) 
Instance details
type Apply (Let6989586621679725985BuildListSym0 :: TyFun k1 (TyFun k2 (TyFun Nat (TyFun [b6989586621679715945] [Nat] -> Type) -> *) -> *) -> *) (l :: k1) = (Let6989586621679725985BuildListSym1 l :: TyFun k2 (TyFun Nat (TyFun [b6989586621679715945] [Nat] -> Type) -> *) -> *)
type Apply (ShowsPrec_6989586621679928121Sym0 :: TyFun Nat (TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928121Sym0 :: TyFun Nat (TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928121Sym1 l :: TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> *)
type Apply (Let6989586621679725985BuildListSym1 l1 :: TyFun k1 (TyFun Nat (TyFun [b6989586621679715945] [Nat] -> Type) -> *) -> *) (l2 :: k1) 
Instance details
type Apply (Let6989586621679725985BuildListSym1 l1 :: TyFun k1 (TyFun Nat (TyFun [b6989586621679715945] [Nat] -> Type) -> *) -> *) (l2 :: k1) = (Let6989586621679725985BuildListSym2 l1 l2 :: TyFun Nat (TyFun [b6989586621679715945] [Nat] -> Type) -> *)
type Apply (Let6989586621679725985BuildListSym2 l1 l2 :: TyFun Nat (TyFun [b6989586621679715945] [Nat] -> Type) -> *) (l3 :: Nat) 
Instance details
type Apply (Let6989586621679725985BuildListSym2 l1 l2 :: TyFun Nat (TyFun [b6989586621679715945] [Nat] -> Type) -> *) (l3 :: Nat) = (Let6989586621679725985BuildListSym3 l1 l2 l3 :: TyFun [b6989586621679715945] [Nat] -> *)
type Apply (ShowsPrec_6989586621679928159Sym0 :: TyFun Nat (TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928159Sym0 :: TyFun Nat (TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928159Sym1 l :: TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrec_6989586621679928198Sym0 :: TyFun Nat (TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928198Sym0 :: TyFun Nat (TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928198Sym1 l :: TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrec_6989586621679928238Sym0 :: TyFun Nat (TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928238Sym0 :: TyFun Nat (TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928238Sym1 l :: TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> *)
type Apply (LengthSym0 :: TyFun [a] Nat -> *) (l :: [a]) 
Instance details
type Apply (LengthSym0 :: TyFun [a] Nat -> *) (l :: [a]) = Length l
type Apply (FindIndicesSym1 l1 :: TyFun [a] [Nat] -> *) (l2 :: [a]) 
Instance details
type Apply (FindIndicesSym1 l1 :: TyFun [a] [Nat] -> *) (l2 :: [a]) = FindIndices l1 l2
type Apply (ElemIndicesSym1 l1 :: TyFun [a] [Nat] -> *) (l2 :: [a]) 
Instance details
type Apply (ElemIndicesSym1 l1 :: TyFun [a] [Nat] -> *) (l2 :: [a]) = ElemIndices l1 l2
type Apply (FindIndexSym1 l1 :: TyFun [a] (Maybe Nat) -> *) (l2 :: [a]) 
Instance details
type Apply (FindIndexSym1 l1 :: TyFun [a] (Maybe Nat) -> *) (l2 :: [a]) = FindIndex l1 l2
type Apply (ElemIndexSym1 l1 :: TyFun [a] (Maybe Nat) -> *) (l2 :: [a]) 
Instance details
type Apply (ElemIndexSym1 l1 :: TyFun [a] (Maybe Nat) -> *) (l2 :: [a]) = ElemIndex l1 l2
type Apply (Let6989586621679725985BuildListSym3 l1 l2 l3 :: TyFun [b6989586621679715945] [Nat] -> *) (l4 :: [b6989586621679715945]) 
Instance details
type Apply (Let6989586621679725985BuildListSym3 l1 l2 l3 :: TyFun [b6989586621679715945] [Nat] -> *) (l4 :: [b6989586621679715945]) = Let6989586621679725985BuildList l1 l2 l3 l4
type Apply ((!!@#@$) :: TyFun [a6989586621679715466] (TyFun Nat a6989586621679715466 -> Type) -> *) (l :: [a6989586621679715466]) 
Instance details
type Apply ((!!@#@$) :: TyFun [a6989586621679715466] (TyFun Nat a6989586621679715466 -> Type) -> *) (l :: [a6989586621679715466]) = (!!@#@$$) l
type Apply (FindIndicesSym0 :: TyFun (TyFun a6989586621679715492 Bool -> Type) (TyFun [a6989586621679715492] [Nat] -> Type) -> *) (l :: TyFun a6989586621679715492 Bool -> Type) 
Instance details
type Apply (FindIndicesSym0 :: TyFun (TyFun a6989586621679715492 Bool -> Type) (TyFun [a6989586621679715492] [Nat] -> Type) -> *) (l :: TyFun a6989586621679715492 Bool -> Type) = FindIndicesSym1 l
type Apply (FindIndexSym0 :: TyFun (TyFun a6989586621679715493 Bool -> Type) (TyFun [a6989586621679715493] (Maybe Nat) -> Type) -> *) (l :: TyFun a6989586621679715493 Bool -> Type) 
Instance details
type Apply (FindIndexSym0 :: TyFun (TyFun a6989586621679715493 Bool -> Type) (TyFun [a6989586621679715493] (Maybe Nat) -> Type) -> *) (l :: TyFun a6989586621679715493 Bool -> Type) = FindIndexSym1 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

Instance details

Associated Types

type DemoteRep Symbol :: *

Methods

fromSing :: Sing a -> DemoteRep Symbol

PShow Symbol 
Instance details

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol

type Show_ arg :: Symbol

type ShowList arg arg1 :: Symbol

SShow Symbol 
Instance details

Methods

sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2)

ShowSing Symbol 
Instance details

Methods

showsSingPrec :: Int -> Sing a -> ShowS

KnownSymbol a => SingI (a :: Symbol)

Since: 4.9.0.0

Instance details

Methods

sing :: Sing a

KnownSymbol n => Reifies (n :: Symbol) String 
Instance details

Methods

reflect :: proxy n -> String

SuppressUnusedWarnings ShowParenSym2 
Instance details
SuppressUnusedWarnings ShowParenSym1 
Instance details
SuppressUnusedWarnings Show_tupleSym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944083Sym2 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944128Sym2 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679928013Sym2 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679943886Sym2 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944174Sym2 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944083Sym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944128Sym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679928013Sym1 
Instance details
SuppressUnusedWarnings ShowsNatSym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679943886Sym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944174Sym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679059182Sym1 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679059182Sym2 
Instance details
SuppressUnusedWarnings ShowCharSym1 
Instance details
SuppressUnusedWarnings ShowStringSym1 
Instance details
SuppressUnusedWarnings (<>@#@$$) 
Instance details
SuppressUnusedWarnings ShowParenSym0 
Instance details
SuppressUnusedWarnings Show_tupleSym0 
Instance details
SuppressUnusedWarnings UnlinesSym0 
Instance details
SuppressUnusedWarnings UnwordsSym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944083Sym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944128Sym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679928013Sym0 
Instance details
SuppressUnusedWarnings ShowsNatSym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679943886Sym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679944174Sym0 
Instance details
SuppressUnusedWarnings ShowsPrec_6989586621679059182Sym0 
Instance details
SuppressUnusedWarnings ShowCharSym0 
Instance details
SuppressUnusedWarnings ShowStringSym0 
Instance details
SuppressUnusedWarnings (<>@#@$) 
Instance details
SuppressUnusedWarnings KnownSymbolSym0 
Instance details
SuppressUnusedWarnings ShowCommaSpaceSym0 
Instance details
SuppressUnusedWarnings ShowSpaceSym0 
Instance details
SuppressUnusedWarnings (ShowListWithSym2 :: (TyFun a6989586621679925816 (TyFun Symbol Symbol -> Type) -> Type) -> [a6989586621679925816] -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowListWithSym1 :: (TyFun a6989586621679925816 (TyFun Symbol Symbol -> Type) -> Type) -> TyFun [a6989586621679925816] (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowList_6989586621679927942Sym1 :: [a6989586621679925832] -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowListSym1 :: [a6989586621679925832] -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927975Sym2 :: Nat -> [a6989586621679925850] -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943933Sym2 :: Nat -> Maybe a3530822107858468865 -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927904Sym2 :: Nat -> a6989586621679925832 -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrecSym2 :: Nat -> a6989586621679925832 -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679944039Sym2 :: Nat -> NonEmpty a6989586621679060556 -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927975Sym1 :: Nat -> TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943933Sym1 :: Nat -> TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927904Sym1 :: Nat -> TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrecSym1 :: Nat -> TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679944039Sym1 :: Nat -> TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsSym1 :: a6989586621679925817 -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (Lambda_6989586621679927686Sym1 :: k -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowListWithSym0 :: TyFun (TyFun a6989586621679925816 (TyFun Symbol Symbol -> Type) -> Type) (TyFun [a6989586621679925816] (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowList_6989586621679927942Sym0 :: TyFun [a6989586621679925832] (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowListSym0 :: TyFun [a6989586621679925832] (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927975Sym0 :: TyFun Nat (TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943933Sym0 :: TyFun Nat (TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679927904Sym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679944039Sym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsSym0 :: TyFun a6989586621679925817 (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (Show__6989586621679927924Sym0 :: TyFun a6989586621679925832 Symbol -> *) 
Instance details
SuppressUnusedWarnings (Show_Sym0 :: TyFun a6989586621679925832 Symbol -> *) 
Instance details
SuppressUnusedWarnings (Lambda_6989586621679927686Sym0 :: TyFun k (TyFun Symbol Symbol -> *) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943989Sym2 :: Nat -> Either a6989586621679082540 b6989586621679082541 -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928048Sym2 :: Nat -> (a6989586621679925854, b6989586621679925855) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943989Sym1 :: Nat -> TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928048Sym1 :: Nat -> TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679725659GoSym2 :: k1 -> k2 -> TyFun [Symbol] Symbol -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679725659GoSym1 :: k1 -> TyFun k2 (TyFun [Symbol] Symbol -> *) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679943989Sym0 :: TyFun Nat (TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928048Sym0 :: TyFun Nat (TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679725659GoSym0 :: TyFun k1 (TyFun k2 (TyFun [Symbol] Symbol -> *) -> *) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928084Sym2 :: Nat -> (a6989586621679925859, b6989586621679925860, c6989586621679925861) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928084Sym1 :: Nat -> TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928084Sym0 :: TyFun Nat (TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679927814ShowlSym0 :: TyFun (k3 ~> (Symbol ~> Symbol)) (TyFun k1 (TyFun k2 (TyFun Symbol (TyFun [k3] Symbol -> *) -> *) -> *) -> *) -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679927814ShowlSym4 :: (k3 ~> (Symbol ~> Symbol)) -> k1 -> k2 -> Symbol -> TyFun [k3] Symbol -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679927814ShowlSym3 :: (k3 ~> (Symbol ~> Symbol)) -> k1 -> k2 -> TyFun Symbol (TyFun [k3] Symbol -> *) -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679927814ShowlSym2 :: (k3 ~> (Symbol ~> Symbol)) -> k1 -> TyFun k2 (TyFun Symbol (TyFun [k3] Symbol -> *) -> *) -> *) 
Instance details
SuppressUnusedWarnings (Let6989586621679927814ShowlSym1 :: (k3 ~> (Symbol ~> Symbol)) -> TyFun k1 (TyFun k2 (TyFun Symbol (TyFun [k3] Symbol -> *) -> *) -> *) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928121Sym2 :: Nat -> (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928121Sym1 :: Nat -> TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (Lambda_6989586621679927770Sym3 :: k1 -> k2 -> (TyFun Symbol c6989586621679694399 -> Type) -> TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) 
Instance details
SuppressUnusedWarnings (Lambda_6989586621679927770Sym2 :: k1 -> k2 -> TyFun (TyFun Symbol c6989586621679694399 -> Type) (TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) -> *) 
Instance details
SuppressUnusedWarnings (Lambda_6989586621679927770Sym1 :: k1 -> TyFun k2 (TyFun (TyFun Symbol c6989586621679694399 -> Type) (TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) -> *) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928121Sym0 :: TyFun Nat (TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (Lambda_6989586621679927770Sym0 :: TyFun k1 (TyFun k2 (TyFun (TyFun Symbol c6989586621679694399 -> Type) (TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) -> *) -> *) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928159Sym2 :: Nat -> (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928159Sym1 :: Nat -> TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928159Sym0 :: TyFun Nat (TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928198Sym2 :: Nat -> (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928198Sym1 :: Nat -> TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928198Sym0 :: TyFun Nat (TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928238Sym2 :: Nat -> (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) -> TyFun Symbol Symbol -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928238Sym1 :: Nat -> TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> *) 
Instance details
SuppressUnusedWarnings (ShowsPrec_6989586621679928238Sym0 :: TyFun Nat (TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> Type) -> *) 
Instance details
data Sing (s :: Symbol) 
Instance details
data Sing (s :: Symbol) where
type DemoteRep Symbol 
Instance details
type DemoteRep Symbol = String
data Sing (n :: Symbol) 
Instance details
data Sing (n :: Symbol) where
type Demote Symbol 
Instance details
type Show_ (arg :: Symbol) 
Instance details
type Show_ (arg :: Symbol) = Apply (Show__6989586621679927924Sym0 :: TyFun Symbol Symbol -> *) arg
type (x :: Symbol) /= (y :: Symbol) 
Instance details
type (x :: Symbol) /= (y :: Symbol) = Not (x == y)
type (a :: Symbol) == (b :: Symbol) 
Instance details
type (a :: Symbol) == (b :: Symbol) = a == b
type (arg1 :: Symbol) < (arg2 :: Symbol) 
Instance details
type (arg1 :: Symbol) < (arg2 :: Symbol) = Apply (Apply (TFHelper_6989586621679569644Sym0 :: TyFun Symbol (TyFun Symbol Bool -> Type) -> *) arg1) arg2
type (arg1 :: Symbol) <= (arg2 :: Symbol) 
Instance details
type (arg1 :: Symbol) <= (arg2 :: Symbol) = Apply (Apply (TFHelper_6989586621679569677Sym0 :: TyFun Symbol (TyFun Symbol Bool -> Type) -> *) arg1) arg2
type (arg1 :: Symbol) > (arg2 :: Symbol) 
Instance details
type (arg1 :: Symbol) > (arg2 :: Symbol) = Apply (Apply (TFHelper_6989586621679569710Sym0 :: TyFun Symbol (TyFun Symbol Bool -> Type) -> *) arg1) arg2
type (arg1 :: Symbol) >= (arg2 :: Symbol) 
Instance details
type (arg1 :: Symbol) >= (arg2 :: Symbol) = Apply (Apply (TFHelper_6989586621679569743Sym0 :: TyFun Symbol (TyFun Symbol Bool -> Type) -> *) arg1) arg2
type Compare (a :: Symbol) (b :: Symbol) 
Instance details
type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b
type Max (arg1 :: Symbol) (arg2 :: Symbol) 
Instance details
type Max (arg1 :: Symbol) (arg2 :: Symbol) = Apply (Apply (Max_6989586621679569776Sym0 :: TyFun Symbol (TyFun Symbol Symbol -> Type) -> *) arg1) arg2
type Min (arg1 :: Symbol) (arg2 :: Symbol) 
Instance details
type Min (arg1 :: Symbol) (arg2 :: Symbol) = Apply (Apply (Min_6989586621679569809Sym0 :: TyFun Symbol (TyFun Symbol Symbol -> Type) -> *) arg1) arg2
type ShowList (arg1 :: [Symbol]) arg2 
Instance details
type ShowList (arg1 :: [Symbol]) arg2 = Apply (Apply (ShowList_6989586621679927942Sym0 :: TyFun [Symbol] (TyFun Symbol Symbol -> Type) -> *) arg1) arg2
type Apply KnownSymbolSym0 (l :: Symbol) 
Instance details
type Apply KnownSymbolSym0 (l :: Symbol) = KnownSymbol l
type Apply ShowCommaSpaceSym0 (l :: Symbol) 
Instance details
type Apply ShowCommaSpaceSym0 (l :: Symbol) = ShowCommaSpace l
type Apply ShowSpaceSym0 (l :: Symbol) 
Instance details
type Apply ShowSpaceSym0 (l :: Symbol) = ShowSpace l
type ShowsPrec a1 (a2 :: Symbol) a3 
Instance details
type ShowsPrec a1 (a2 :: Symbol) a3 = Apply (Apply (Apply ShowsPrec_6989586621679928013Sym0 a1) a2) a3
type Apply (ShowCharSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) 
Instance details
type Apply (ShowCharSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = ShowChar l1 l2
type Apply (ShowStringSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) 
Instance details
type Apply (ShowStringSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = ShowString l1 l2
type Apply ((<>@#@$$) l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) 
Instance details
type Apply ((<>@#@$$) l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = l1 <> l2
type Apply (Show_tupleSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) 
Instance details
type Apply (Show_tupleSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = Show_tuple l1 l2
type Apply (ShowsNatSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) 
Instance details
type Apply (ShowsNatSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = ShowsNat l1 l2
type Apply (Show__6989586621679927924Sym0 :: TyFun a Symbol -> *) (l :: a) 
Instance details
type Apply (Show__6989586621679927924Sym0 :: TyFun a Symbol -> *) (l :: a) = Show__6989586621679927924 l
type Apply (Show_Sym0 :: TyFun a Symbol -> *) (l :: a) 
Instance details
type Apply (Show_Sym0 :: TyFun a Symbol -> *) (l :: a) = Show_ l
type Apply (ShowListSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) 
Instance details
type Apply (ShowListSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = ShowList l1 l2
type Apply (ShowParenSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowParenSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowParen l1 l2 l3
type Apply (ShowsSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) 
Instance details
type Apply (ShowsSym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = Shows l1 l2
type Apply (Lambda_6989586621679927686Sym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) 
Instance details
type Apply (Lambda_6989586621679927686Sym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = Lambda_6989586621679927686 l1 l2
type Apply (ShowList_6989586621679927942Sym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) 
Instance details
type Apply (ShowList_6989586621679927942Sym1 l1 :: TyFun Symbol Symbol -> *) (l2 :: Symbol) = ShowList_6989586621679927942 l1 l2
type Apply (ShowsPrec_6989586621679928013Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679928013Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679928013 l1 l2 l3
type Apply (ShowsPrec_6989586621679943886Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679943886Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679943886 l1 l2 l3
type Apply (ShowsPrec_6989586621679944083Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679944083Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679944083 l1 l2 l3
type Apply (ShowsPrec_6989586621679944128Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679944128Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679944128 l1 l2 l3
type Apply (ShowsPrec_6989586621679944174Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679944174Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679944174 l1 l2 l3
type Apply (ShowsPrec_6989586621679059182Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679059182Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679059182 l1 l2 l3
type Apply (ShowsPrecSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrecSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec l1 l2 l3
type Apply (ShowListWithSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowListWithSym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowListWith l1 l2 l3
type Apply (ShowsPrec_6989586621679927904Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679927904Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679927904 l1 l2 l3
type Apply (ShowsPrec_6989586621679927975Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679927975Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679927975 l1 l2 l3
type Apply (ShowsPrec_6989586621679943933Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679943933Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679943933 l1 l2 l3
type Apply (ShowsPrec_6989586621679944039Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679944039Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679944039 l1 l2 l3
type Apply (ShowsPrec_6989586621679928048Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679928048Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679928048 l1 l2 l3
type Apply (ShowsPrec_6989586621679943989Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679943989Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679943989 l1 l2 l3
type Apply (ShowsPrec_6989586621679928084Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679928084Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679928084 l1 l2 l3
type Apply (ShowsPrec_6989586621679928121Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679928121Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679928121 l1 l2 l3
type Apply (ShowsPrec_6989586621679928159Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679928159Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679928159 l1 l2 l3
type Apply (ShowsPrec_6989586621679928198Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679928198Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679928198 l1 l2 l3
type Apply (ShowsPrec_6989586621679928238Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679928238Sym2 l1 l2 :: TyFun Symbol Symbol -> *) (l3 :: Symbol) = ShowsPrec_6989586621679928238 l1 l2 l3
type Apply ShowParenSym0 (l :: Bool) 
Instance details
type Apply ShowParenSym0 (l :: Bool) = ShowParenSym1 l
type Apply ShowsPrec_6989586621679944083Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679944083Sym0 (l :: Nat) = ShowsPrec_6989586621679944083Sym1 l
type Apply ShowsPrec_6989586621679944128Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679944128Sym0 (l :: Nat) = ShowsPrec_6989586621679944128Sym1 l
type Apply ShowsPrec_6989586621679928013Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679928013Sym0 (l :: Nat) = ShowsPrec_6989586621679928013Sym1 l
type Apply ShowsNatSym0 (l :: Nat) 
Instance details
type Apply ShowsNatSym0 (l :: Nat) = ShowsNatSym1 l
type Apply ShowsPrec_6989586621679943886Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679943886Sym0 (l :: Nat) = ShowsPrec_6989586621679943886Sym1 l
type Apply ShowsPrec_6989586621679944174Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679944174Sym0 (l :: Nat) = ShowsPrec_6989586621679944174Sym1 l
type Apply ShowsPrec_6989586621679059182Sym0 (l :: Nat) 
Instance details
type Apply ShowsPrec_6989586621679059182Sym0 (l :: Nat) = ShowsPrec_6989586621679059182Sym1 l
type Apply ShowCharSym0 (l :: Symbol) 
Instance details
type Apply ShowCharSym0 (l :: Symbol) = ShowCharSym1 l
type Apply ShowStringSym0 (l :: Symbol) 
Instance details
type Apply ShowStringSym0 (l :: Symbol) = ShowStringSym1 l
type Apply (<>@#@$) (l :: Symbol) 
Instance details
type Apply (<>@#@$) (l :: Symbol) = (<>@#@$$) l
type Apply (ShowsPrec_6989586621679944083Sym1 l1 :: TyFun Bool (TyFun Symbol Symbol -> Type) -> *) (l2 :: Bool) 
Instance details
type Apply (ShowsPrec_6989586621679944083Sym1 l1 :: TyFun Bool (TyFun Symbol Symbol -> Type) -> *) (l2 :: Bool) = ShowsPrec_6989586621679944083Sym2 l1 l2
type Apply (ShowsPrec_6989586621679944128Sym1 l1 :: TyFun Ordering (TyFun Symbol Symbol -> Type) -> *) (l2 :: Ordering) 
Instance details
type Apply (ShowsPrec_6989586621679944128Sym1 l1 :: TyFun Ordering (TyFun Symbol Symbol -> Type) -> *) (l2 :: Ordering) = ShowsPrec_6989586621679944128Sym2 l1 l2
type Apply (ShowsPrec_6989586621679927975Sym0 :: TyFun Nat (TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679927975Sym0 :: TyFun Nat (TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679927975Sym1 l :: TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrec_6989586621679943933Sym0 :: TyFun Nat (TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679943933Sym0 :: TyFun Nat (TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679943933Sym1 l :: TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrec_6989586621679927904Sym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679927904Sym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679927904Sym1 l :: TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrecSym0 :: TyFun Nat (TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrecSym1 l :: TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrec_6989586621679944039Sym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679944039Sym0 :: TyFun Nat (TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679944039Sym1 l :: TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrec_6989586621679928013Sym1 l1 :: TyFun Symbol (TyFun Symbol Symbol -> Type) -> *) (l2 :: Symbol) 
Instance details
type Apply (ShowsPrec_6989586621679928013Sym1 l1 :: TyFun Symbol (TyFun Symbol Symbol -> Type) -> *) (l2 :: Symbol) = ShowsPrec_6989586621679928013Sym2 l1 l2
type Apply (ShowsPrec_6989586621679943886Sym1 l1 :: TyFun () (TyFun Symbol Symbol -> Type) -> *) (l2 :: ()) 
Instance details
type Apply (ShowsPrec_6989586621679943886Sym1 l1 :: TyFun () (TyFun Symbol Symbol -> Type) -> *) (l2 :: ()) = ShowsPrec_6989586621679943886Sym2 l1 l2
type Apply (Lambda_6989586621679927686Sym0 :: TyFun k (TyFun Symbol Symbol -> *) -> *) (l :: k) 
Instance details
type Apply (Lambda_6989586621679927686Sym0 :: TyFun k (TyFun Symbol Symbol -> *) -> *) (l :: k) = Lambda_6989586621679927686Sym1 l
type Apply (ShowsSym0 :: TyFun a6989586621679925817 (TyFun Symbol Symbol -> Type) -> *) (l :: a6989586621679925817) 
Instance details
type Apply (ShowsSym0 :: TyFun a6989586621679925817 (TyFun Symbol Symbol -> Type) -> *) (l :: a6989586621679925817) = ShowsSym1 l
type Apply (ShowsPrec_6989586621679944174Sym1 l1 :: TyFun Void (TyFun Symbol Symbol -> Type) -> *) (l2 :: Void) 
Instance details
type Apply (ShowsPrec_6989586621679944174Sym1 l1 :: TyFun Void (TyFun Symbol Symbol -> Type) -> *) (l2 :: Void) = ShowsPrec_6989586621679944174Sym2 l1 l2
type Apply (ShowsPrec_6989586621679059182Sym1 l1 :: TyFun Nat (TyFun Symbol Symbol -> Type) -> *) (l2 :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679059182Sym1 l1 :: TyFun Nat (TyFun Symbol Symbol -> Type) -> *) (l2 :: Nat) = ShowsPrec_6989586621679059182Sym2 l1 l2
type Apply (ShowsPrec_6989586621679943989Sym0 :: TyFun Nat (TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679943989Sym0 :: TyFun Nat (TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679943989Sym1 l :: TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrec_6989586621679928048Sym0 :: TyFun Nat (TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928048Sym0 :: TyFun Nat (TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928048Sym1 l :: TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> *)
type Apply (ShowsPrec_6989586621679927904Sym1 l1 :: TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *) (l2 :: a6989586621679925832) 
Instance details
type Apply (ShowsPrec_6989586621679927904Sym1 l1 :: TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *) (l2 :: a6989586621679925832) = ShowsPrec_6989586621679927904Sym2 l1 l2
type Apply (ShowsPrecSym1 l1 :: TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *) (l2 :: a6989586621679925832) 
Instance details
type Apply (ShowsPrecSym1 l1 :: TyFun a6989586621679925832 (TyFun Symbol Symbol -> Type) -> *) (l2 :: a6989586621679925832) = ShowsPrecSym2 l1 l2
type Apply (Let6989586621679725659GoSym0 :: TyFun k1 (TyFun k2 (TyFun [Symbol] Symbol -> *) -> *) -> *) (l :: k1) 
Instance details
type Apply (Let6989586621679725659GoSym0 :: TyFun k1 (TyFun k2 (TyFun [Symbol] Symbol -> *) -> *) -> *) (l :: k1) = (Let6989586621679725659GoSym1 l :: TyFun k2 (TyFun [Symbol] Symbol -> *) -> *)
type Apply (ShowsPrec_6989586621679928084Sym0 :: TyFun Nat (TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928084Sym0 :: TyFun Nat (TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928084Sym1 l :: TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> *)
type Apply (Let6989586621679725659GoSym1 l1 :: TyFun k1 (TyFun [Symbol] Symbol -> *) -> *) (l2 :: k1) 
Instance details
type Apply (Let6989586621679725659GoSym1 l1 :: TyFun k1 (TyFun [Symbol] Symbol -> *) -> *) (l2 :: k1) = Let6989586621679725659GoSym2 l1 l2
type Apply (ShowsPrec_6989586621679928121Sym0 :: TyFun Nat (TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928121Sym0 :: TyFun Nat (TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928121Sym1 l :: TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> *)
type Apply (Let6989586621679927814ShowlSym1 l1 :: TyFun k1 (TyFun k3 (TyFun Symbol (TyFun [k2] Symbol -> *) -> *) -> *) -> *) (l2 :: k1) 
Instance details
type Apply (Let6989586621679927814ShowlSym1 l1 :: TyFun k1 (TyFun k3 (TyFun Symbol (TyFun [k2] Symbol -> *) -> *) -> *) -> *) (l2 :: k1) = (Let6989586621679927814ShowlSym2 l1 l2 :: TyFun k3 (TyFun Symbol (TyFun [k2] Symbol -> *) -> *) -> *)
type Apply (Lambda_6989586621679927770Sym0 :: TyFun k1 (TyFun k2 (TyFun (TyFun Symbol c6989586621679694399 -> Type) (TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) -> *) -> *) -> *) (l :: k1) 
Instance details
type Apply (Lambda_6989586621679927770Sym0 :: TyFun k1 (TyFun k2 (TyFun (TyFun Symbol c6989586621679694399 -> Type) (TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) -> *) -> *) -> *) (l :: k1) = (Lambda_6989586621679927770Sym1 l :: TyFun k2 (TyFun (TyFun Symbol c6989586621679694399 -> Type) (TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) -> *) -> *)
type Apply (ShowsPrec_6989586621679928159Sym0 :: TyFun Nat (TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928159Sym0 :: TyFun Nat (TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928159Sym1 l :: TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> *)
type Apply (Let6989586621679927814ShowlSym2 l1 l2 :: TyFun k3 (TyFun Symbol (TyFun [k2] Symbol -> *) -> *) -> *) (l3 :: k3) 
Instance details
type Apply (Let6989586621679927814ShowlSym2 l1 l2 :: TyFun k3 (TyFun Symbol (TyFun [k2] Symbol -> *) -> *) -> *) (l3 :: k3) = Let6989586621679927814ShowlSym3 l1 l2 l3
type Apply (Lambda_6989586621679927770Sym1 l1 :: TyFun k1 (TyFun (TyFun Symbol c6989586621679694399 -> Type) (TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) -> *) -> *) (l2 :: k1) 
Instance details
type Apply (Lambda_6989586621679927770Sym1 l1 :: TyFun k1 (TyFun (TyFun Symbol c6989586621679694399 -> Type) (TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) -> *) -> *) (l2 :: k1) = (Lambda_6989586621679927770Sym2 l1 l2 :: TyFun (TyFun Symbol c6989586621679694399 -> Type) (TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) -> *)
type Apply (ShowsPrec_6989586621679928198Sym0 :: TyFun Nat (TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928198Sym0 :: TyFun Nat (TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928198Sym1 l :: TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> *)
type Apply (Let6989586621679927814ShowlSym3 l1 l2 l3 :: TyFun Symbol (TyFun [k2] Symbol -> *) -> *) (l4 :: Symbol) 
Instance details
type Apply (Let6989586621679927814ShowlSym3 l1 l2 l3 :: TyFun Symbol (TyFun [k2] Symbol -> *) -> *) (l4 :: Symbol) = Let6989586621679927814ShowlSym4 l1 l2 l3 l4
type Apply (ShowsPrec_6989586621679928238Sym0 :: TyFun Nat (TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) 
Instance details
type Apply (ShowsPrec_6989586621679928238Sym0 :: TyFun Nat (TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: Nat) = (ShowsPrec_6989586621679928238Sym1 l :: TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> *)
type Apply UnlinesSym0 (l :: [Symbol]) 
Instance details
type Apply UnlinesSym0 (l :: [Symbol]) = Unlines l
type Apply UnwordsSym0 (l :: [Symbol]) 
Instance details
type Apply UnwordsSym0 (l :: [Symbol]) = Unwords l
type Apply (Let6989586621679725659GoSym2 l1 l2 :: TyFun [Symbol] Symbol -> *) (l3 :: [Symbol]) 
Instance details
type Apply (Let6989586621679725659GoSym2 l1 l2 :: TyFun [Symbol] Symbol -> *) (l3 :: [Symbol]) = Let6989586621679725659Go l1 l2 l3
type Apply (Let6989586621679927814ShowlSym4 l1 l2 l3 l4 :: TyFun [k2] Symbol -> *) (l5 :: [k2]) 
Instance details
type Apply (Let6989586621679927814ShowlSym4 l1 l2 l3 l4 :: TyFun [k2] Symbol -> *) (l5 :: [k2]) = Let6989586621679927814Showl l1 l2 l3 l4 l5
type Apply Show_tupleSym0 (l :: [TyFun Symbol Symbol -> Type]) 
Instance details
type Apply Show_tupleSym0 (l :: [TyFun Symbol Symbol -> Type]) = Show_tupleSym1 l
type Apply (ShowList_6989586621679927942Sym0 :: TyFun [a6989586621679925832] (TyFun Symbol Symbol -> Type) -> *) (l :: [a6989586621679925832]) 
Instance details
type Apply (ShowList_6989586621679927942Sym0 :: TyFun [a6989586621679925832] (TyFun Symbol Symbol -> Type) -> *) (l :: [a6989586621679925832]) = ShowList_6989586621679927942Sym1 l
type Apply (ShowListSym0 :: TyFun [a6989586621679925832] (TyFun Symbol Symbol -> Type) -> *) (l :: [a6989586621679925832]) 
Instance details
type Apply (ShowListSym0 :: TyFun [a6989586621679925832] (TyFun Symbol Symbol -> Type) -> *) (l :: [a6989586621679925832]) = ShowListSym1 l
type Apply (ShowListWithSym1 l1 :: TyFun [a6989586621679925816] (TyFun Symbol Symbol -> Type) -> *) (l2 :: [a6989586621679925816]) 
Instance details
type Apply (ShowListWithSym1 l1 :: TyFun [a6989586621679925816] (TyFun Symbol Symbol -> Type) -> *) (l2 :: [a6989586621679925816]) = ShowListWithSym2 l1 l2
type Apply (ShowsPrec_6989586621679927975Sym1 l1 :: TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> *) (l2 :: [a6989586621679925850]) 
Instance details
type Apply (ShowsPrec_6989586621679927975Sym1 l1 :: TyFun [a6989586621679925850] (TyFun Symbol Symbol -> Type) -> *) (l2 :: [a6989586621679925850]) = ShowsPrec_6989586621679927975Sym2 l1 l2
type Apply (ShowsPrec_6989586621679943933Sym1 l1 :: TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> *) (l2 :: Maybe a3530822107858468865) 
Instance details
type Apply (ShowsPrec_6989586621679943933Sym1 l1 :: TyFun (Maybe a3530822107858468865) (TyFun Symbol Symbol -> Type) -> *) (l2 :: Maybe a3530822107858468865) = ShowsPrec_6989586621679943933Sym2 l1 l2
type Apply (ShowsPrec_6989586621679944039Sym1 l1 :: TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> *) (l2 :: NonEmpty a6989586621679060556) 
Instance details
type Apply (ShowsPrec_6989586621679944039Sym1 l1 :: TyFun (NonEmpty a6989586621679060556) (TyFun Symbol Symbol -> Type) -> *) (l2 :: NonEmpty a6989586621679060556) = ShowsPrec_6989586621679944039Sym2 l1 l2
type Apply (ShowParenSym1 l1 :: TyFun (TyFun Symbol Symbol -> Type) (TyFun Symbol Symbol -> Type) -> *) (l2 :: TyFun Symbol Symbol -> Type) 
Instance details
type Apply (ShowParenSym1 l1 :: TyFun (TyFun Symbol Symbol -> Type) (TyFun Symbol Symbol -> Type) -> *) (l2 :: TyFun Symbol Symbol -> Type) = ShowParenSym2 l1 l2
type Apply (ShowListWithSym0 :: TyFun (TyFun a6989586621679925816 (TyFun Symbol Symbol -> Type) -> Type) (TyFun [a6989586621679925816] (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: TyFun a6989586621679925816 (TyFun Symbol Symbol -> Type) -> Type) 
Instance details
type Apply (ShowListWithSym0 :: TyFun (TyFun a6989586621679925816 (TyFun Symbol Symbol -> Type) -> Type) (TyFun [a6989586621679925816] (TyFun Symbol Symbol -> Type) -> Type) -> *) (l :: TyFun a6989586621679925816 (TyFun Symbol Symbol -> Type) -> Type) = ShowListWithSym1 l
type Apply (ShowsPrec_6989586621679943989Sym1 l1 :: TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> *) (l2 :: Either a6989586621679082540 b6989586621679082541) 
Instance details
type Apply (ShowsPrec_6989586621679943989Sym1 l1 :: TyFun (Either a6989586621679082540 b6989586621679082541) (TyFun Symbol Symbol -> Type) -> *) (l2 :: Either a6989586621679082540 b6989586621679082541) = ShowsPrec_6989586621679943989Sym2 l1 l2
type Apply (ShowsPrec_6989586621679928048Sym1 l1 :: TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925854, b6989586621679925855)) 
Instance details
type Apply (ShowsPrec_6989586621679928048Sym1 l1 :: TyFun (a6989586621679925854, b6989586621679925855) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925854, b6989586621679925855)) = ShowsPrec_6989586621679928048Sym2 l1 l2
type Apply (Let6989586621679927814ShowlSym0 :: TyFun (k1 ~> (Symbol ~> Symbol)) (TyFun k2 (TyFun k3 (TyFun Symbol (TyFun [k1] Symbol -> *) -> *) -> *) -> *) -> *) (l :: k1 ~> (Symbol ~> Symbol)) 
Instance details
type Apply (Let6989586621679927814ShowlSym0 :: TyFun (k1 ~> (Symbol ~> Symbol)) (TyFun k2 (TyFun k3 (TyFun Symbol (TyFun [k1] Symbol -> *) -> *) -> *) -> *) -> *) (l :: k1 ~> (Symbol ~> Symbol)) = (Let6989586621679927814ShowlSym1 l :: TyFun k2 (TyFun k3 (TyFun Symbol (TyFun [k1] Symbol -> *) -> *) -> *) -> *)
type Apply (Lambda_6989586621679927770Sym2 l1 l2 :: TyFun (TyFun Symbol c6989586621679694399 -> Type) (TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) -> *) (l3 :: TyFun Symbol c6989586621679694399 -> Type) 
Instance details
type Apply (Lambda_6989586621679927770Sym2 l1 l2 :: TyFun (TyFun Symbol c6989586621679694399 -> Type) (TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) -> *) (l3 :: TyFun Symbol c6989586621679694399 -> Type) = (Lambda_6989586621679927770Sym3 l1 l2 l3 :: TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *)
type Apply (Lambda_6989586621679927770Sym3 l1 l2 l3 :: TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) (l4 :: TyFun a6989586621679694400 Symbol -> Type) 
Instance details
type Apply (Lambda_6989586621679927770Sym3 l1 l2 l3 :: TyFun (TyFun a6989586621679694400 Symbol -> Type) (TyFun a6989586621679694400 c6989586621679694399 -> Type) -> *) (l4 :: TyFun a6989586621679694400 Symbol -> Type) = Lambda_6989586621679927770 l1 l2 l3 l4
type Apply (ShowsPrec_6989586621679928084Sym1 l1 :: TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925859, b6989586621679925860, c6989586621679925861)) 
Instance details
type Apply (ShowsPrec_6989586621679928084Sym1 l1 :: TyFun (a6989586621679925859, b6989586621679925860, c6989586621679925861) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925859, b6989586621679925860, c6989586621679925861)) = ShowsPrec_6989586621679928084Sym2 l1 l2
type Apply (ShowsPrec_6989586621679928121Sym1 l1 :: TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869)) 
Instance details
type Apply (ShowsPrec_6989586621679928121Sym1 l1 :: TyFun (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925866, b6989586621679925867, c6989586621679925868, d6989586621679925869)) = ShowsPrec_6989586621679928121Sym2 l1 l2
type Apply (ShowsPrec_6989586621679928159Sym1 l1 :: TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879)) 
Instance details
type Apply (ShowsPrec_6989586621679928159Sym1 l1 :: TyFun (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925875, b6989586621679925876, c6989586621679925877, d6989586621679925878, e6989586621679925879)) = ShowsPrec_6989586621679928159Sym2 l1 l2
type Apply (ShowsPrec_6989586621679928198Sym1 l1 :: TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891)) 
Instance details
type Apply (ShowsPrec_6989586621679928198Sym1 l1 :: TyFun (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925886, b6989586621679925887, c6989586621679925888, d6989586621679925889, e6989586621679925890, f6989586621679925891)) = ShowsPrec_6989586621679928198Sym2 l1 l2
type Apply (ShowsPrec_6989586621679928238Sym1 l1 :: TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905)) 
Instance details
type Apply (ShowsPrec_6989586621679928238Sym1 l1 :: TyFun (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905) (TyFun Symbol Symbol -> Type) -> *) (l2 :: (a6989586621679925899, b6989586621679925900, c6989586621679925901, d6989586621679925902, e6989586621679925903, f6989586621679925904, g6989586621679925905)) = ShowsPrec_6989586621679928238Sym2 l1 l2

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #

Exponentiation of type-level naturals.

Since: 4.7.0.0

type family (a :: Nat) <=? (b :: Nat) :: Bool where ... infix 4 #

Comparison of type-level naturals, as a function. NOTE: The functionality for this function should be subsumed by CmpNat, so this might go away in the future. Please let us know, if you encounter discrepancies between the two.

type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ... #

Comparison of type-level symbols, as a function.

Since: 4.7.0.0

type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ... #

Comparison of type-level naturals, as a function.

Since: 4.7.0.0

type family Div (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #

Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).

Since: 4.11.0.0

type family Mod (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Since: 4.11.0.0

type family Log2 (a :: Nat) :: Nat where ... #

Log base 2 (round down) of natural numbers. Log 0 is undefined (i.e., it cannot be reduced).

Since: 4.11.0.0

type family TypeError (a :: ErrorMessage) :: b where ... #

The type-level equivalent of error.

The polymorphic kind of this type allows it to be used in several settings. For instance, it can be used as a constraint, e.g. to provide a better error message for a non-existent instance,

-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
                    Text "Perhaps there is a missing argument?")
      => Show (a -> b) where
    showsPrec = error "unreachable"

It can also be placed on the right-hand side of a type-level function to provide an error for an invalid case,

type family ByteSize x where
   ByteSize Word16   = 2
   ByteSize Word8    = 1
   ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
                                  Text " is not exportable.")

Since: 4.9.0.0

type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol where ... #

Concatenation of type-level symbols.

Since: 4.10.0.0

sameSymbol :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b) #

We either get evidence that this function was instantiated with the same type-level symbols, or Nothing.

Since: 4.7.0.0

someSymbolVal :: String -> SomeSymbol #

Convert a string into an unknown type-level symbol.

Since: 4.7.0.0

someNatVal :: Integer -> Maybe SomeNat #

Convert an integer into an unknown type-level natural.

Since: 4.7.0.0

symbolVal' :: KnownSymbol n => Proxy# n -> String #

Since: 4.8.0.0

natVal' :: KnownNat n => Proxy# n -> Integer #

Since: 4.8.0.0

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

Since: 4.7.0.0

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

Since: 4.7.0.0

data SomeSymbol where #

This type represents unknown type-level symbols.

Constructors

SomeSymbol :: SomeSymbol

Since: 4.7.0.0

Instances
Eq SomeSymbol

Since: 4.7.0.0

Instance details
Ord SomeSymbol

Since: 4.7.0.0

Instance details
Read SomeSymbol

Since: 4.7.0.0

Instance details
Show SomeSymbol

Since: 4.7.0.0

Instance details

data ErrorMessage where #

A description of a custom type error.

Constructors

Text :: ErrorMessage

Show the text as is.

ShowType :: ErrorMessage

Pretty print the type. ShowType :: k -> ErrorMessage

(:<>:) :: ErrorMessage infixl 6

Put two pieces of error message next to each other.

(:$$:) :: ErrorMessage infixl 5

Stack two pieces of error message on top of each other.

sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) #

We either get evidence that this function was instantiated with the same type-level numbers, or Nothing.

Since: 4.7.0.0

data SomeNat where #

This type represents unknown type-level natural numbers.

Since: 4.10.0.0

Constructors

SomeNat :: SomeNat 
Instances
Eq SomeNat

Since: 4.7.0.0

Instance details

Methods

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

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

Ord SomeNat

Since: 4.7.0.0

Instance details
Read SomeNat

Since: 4.7.0.0

Instance details
Show SomeNat

Since: 4.7.0.0

Instance details

withSingI :: Sing n -> (SingI n -> r) -> r #

data family Sing (a :: k) :: * #

Instances
ShowSing Nat => Show (Sing z) 
Instance details

Methods

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

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

data Sing (z :: Bool) 
Instance details
data Sing (z :: Bool) where
data Sing (z :: Ordering) 
Instance details
data Sing (z :: Ordering) where
data Sing (n :: Nat) 
Instance details
data Sing (n :: Nat) where
data Sing (n :: Symbol) 
Instance details
data Sing (n :: Symbol) where
data Sing (z :: ()) 
Instance details
data Sing (z :: ()) where
data Sing (z :: Void) 
Instance details
data Sing (z :: Void)
data Sing (z :: Nat) 
Instance details
data Sing (z :: Nat) where
data Sing (z :: [a]) 
Instance details
data Sing (z :: [a]) where
data Sing (z :: Maybe a) 
Instance details
data Sing (z :: Maybe a) where
data Sing (z :: NonEmpty a) 
Instance details
data Sing (z :: NonEmpty a) where
data Sing (z :: Either a b) 
Instance details
data Sing (z :: Either a b) where
data Sing (z :: (a, b)) 
Instance details
data Sing (z :: (a, b)) where
data Sing (f :: k1 ~> k2) 
Instance details
data Sing (f :: k1 ~> k2) = SLambda {}
data Sing (z :: (a, b, c)) 
Instance details
data Sing (z :: (a, b, c)) where
data Sing (z :: (a, b, c, d)) 
Instance details
data Sing (z :: (a, b, c, d)) where
data Sing (z :: (a, b, c, d, e)) 
Instance details
data Sing (z :: (a, b, c, d, e)) where
data Sing (z :: (a, b, c, d, e, f)) 
Instance details
data Sing (z :: (a, b, c, d, e, f)) where
data Sing (z :: (a, b, c, d, e, f, g)) 
Instance details
data Sing (z :: (a, b, c, d, e, f, g)) where

class SingI (a :: k) where #

Minimal complete definition

sing

Methods

sing :: Sing a #

Instances
SingI Z 
Instance details

Methods

sing :: Sing Z #

SingI n => SingI (S n :: Nat) 
Instance details

Methods

sing :: Sing (S n) #

class SingKind k where #

Minimal complete definition

fromSing, toSing

Associated Types

type Demote k = (r :: *) | r -> k #

Methods

fromSing :: Sing a -> Demote k #

toSing :: Demote k -> SomeSing k #

Instances
SingKind Nat 
Instance details

Associated Types

type Demote Nat = (r :: *) #

Methods

fromSing :: Sing a -> Demote Nat #

toSing :: Demote Nat -> SomeSing Nat #

(SingKind k1, SingKind k2) => SingKind (k1 ~> k2) 
Instance details

Associated Types

type Demote (k1 ~> k2) = (r :: *) #

Methods

fromSing :: Sing a -> Demote (k1 ~> k2) #

toSing :: Demote (k1 ~> k2) -> SomeSing (k1 ~> k2) #

data SomeSing k where #

Constructors

SomeSing :: SomeSing k 

class PEnum a #

Associated Types

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

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

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

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

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

type EnumFromThenTo (arg :: a) (arg1 :: a) (arg2 :: a) :: [a] #

Instances
PEnum Bool 
Instance details

Associated Types

type Succ arg :: a #

type Pred arg :: a #

type ToEnum arg :: a #

type FromEnum arg :: Nat #

type EnumFromTo arg arg1 :: [a] #

type EnumFromThenTo arg arg1 arg2 :: [a] #

PEnum Ordering 
Instance details

Associated Types

type Succ arg :: a #

type Pred arg :: a #

type ToEnum arg :: a #

type FromEnum arg :: Nat #

type EnumFromTo arg arg1 :: [a] #

type EnumFromThenTo arg arg1 arg2 :: [a] #

PEnum Nat 
Instance details

Associated Types

type Succ arg :: a #

type Pred arg :: a #

type ToEnum arg :: a #

type FromEnum arg :: Nat #

type EnumFromTo arg arg1 :: [a] #

type EnumFromThenTo arg arg1 arg2 :: [a] #

PEnum () 
Instance details

Associated Types

type Succ arg :: a #

type Pred arg :: a #

type ToEnum arg :: a #

type FromEnum arg :: Nat #

type EnumFromTo arg arg1 :: [a] #

type EnumFromThenTo arg arg1 arg2 :: [a] #

PEnum Nat 
Instance details

Associated Types

type Succ arg :: a #

type Pred arg :: a #

type ToEnum arg :: a #

type FromEnum arg :: Nat #

type EnumFromTo arg arg1 :: [a] #

type EnumFromThenTo arg arg1 arg2 :: [a] #

class SEnum a where #

Minimal complete definition

sToEnum, sFromEnum

Methods

sSucc :: Sing t -> Sing (Apply (SuccSym0 :: TyFun a a -> *) t) #

sPred :: Sing t -> Sing (Apply (PredSym0 :: TyFun a a -> *) t) #

sToEnum :: Sing t -> Sing (Apply (ToEnumSym0 :: TyFun Nat a -> *) t) #

sFromEnum :: Sing t -> Sing (Apply (FromEnumSym0 :: TyFun a Nat -> *) t) #

sEnumFromTo :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (EnumFromToSym0 :: TyFun a (TyFun a [a] -> Type) -> *) t1) t2) #

sEnumFromThenTo :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (EnumFromThenToSym0 :: TyFun a (TyFun a (TyFun a [a] -> Type) -> Type) -> *) t1) t2) t3) #

Instances
SEnum Bool 
Instance details

Methods

sSucc :: Sing t -> Sing (Apply SuccSym0 t) #

sPred :: Sing t -> Sing (Apply PredSym0 t) #

sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) #

sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) #

sEnumFromTo :: Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2) #

sEnumFromThenTo :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3) #

SEnum Ordering 
Instance details

Methods

sSucc :: Sing t -> Sing (Apply SuccSym0 t) #

sPred :: Sing t -> Sing (Apply PredSym0 t) #

sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) #

sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) #

sEnumFromTo :: Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2) #

sEnumFromThenTo :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3) #

SEnum Nat 
Instance details

Methods

sSucc :: Sing t -> Sing (Apply SuccSym0 t) #

sPred :: Sing t -> Sing (Apply PredSym0 t) #

sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) #

sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) #

sEnumFromTo :: Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2) #

sEnumFromThenTo :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3) #

SEnum () 
Instance details

Methods

sSucc :: Sing t -> Sing (Apply SuccSym0 t) #

sPred :: Sing t -> Sing (Apply PredSym0 t) #

sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) #

sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) #

sEnumFromTo :: Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2) #

sEnumFromThenTo :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3) #

SEnum Nat 
Instance details

Methods

sSucc :: Sing t -> Sing (Apply SuccSym0 t) #

sPred :: Sing t -> Sing (Apply PredSym0 t) #

sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) #

sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) #

sEnumFromTo :: Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2) #

sEnumFromThenTo :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3) #

data (/=@#@$) (l :: TyFun a6989586621679557194 (TyFun a6989586621679557194 Bool -> Type)) :: forall a6989586621679557194. TyFun a6989586621679557194 (TyFun a6989586621679557194 Bool -> Type) -> * #

Instances
SuppressUnusedWarnings ((/=@#@$) :: TyFun a6989586621679557194 (TyFun a6989586621679557194 Bool -> Type) -> *) 
Instance details
type Apply ((/=@#@$) :: TyFun a6989586621679557194 (TyFun a6989586621679557194 Bool -> Type) -> *) (l :: a6989586621679557194) 
Instance details
type Apply ((/=@#@$) :: TyFun a6989586621679557194 (TyFun a6989586621679557194 Bool -> Type) -> *) (l :: a6989586621679557194) = (/=@#@$$) l

data (l :: a6989586621679557194) /=@#@$$ (l1 :: TyFun a6989586621679557194 Bool) :: forall a6989586621679557194. a6989586621679557194 -> TyFun a6989586621679557194 Bool -> * #

Instances
SuppressUnusedWarnings ((/=@#@$$) :: a6989586621679557194 -> TyFun a6989586621679557194 Bool -> *) 
Instance details
type Apply ((/=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) 
Instance details
type Apply ((/=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 /= l2

type (/=@#@$$$) (t :: a6989586621679557194) (t1 :: a6989586621679557194) = t /= t1 #

data (==@#@$) (l :: TyFun a6989586621679557194 (TyFun a6989586621679557194 Bool -> Type)) :: forall a6989586621679557194. TyFun a6989586621679557194 (TyFun a6989586621679557194 Bool -> Type) -> * #

Instances
SuppressUnusedWarnings ((==@#@$) :: TyFun a6989586621679557194 (TyFun a6989586621679557194 Bool -> Type) -> *) 
Instance details
type Apply ((==@#@$) :: TyFun a6989586621679557194 (TyFun a6989586621679557194 Bool -> Type) -> *) (l :: a6989586621679557194) 
Instance details
type Apply ((==@#@$) :: TyFun a6989586621679557194 (TyFun a6989586621679557194 Bool -> Type) -> *) (l :: a6989586621679557194) = (==@#@$$) l

data (l :: a6989586621679557194) ==@#@$$ (l1 :: TyFun a6989586621679557194 Bool) :: forall a6989586621679557194. a6989586621679557194 -> TyFun a6989586621679557194 Bool -> * #

Instances
SuppressUnusedWarnings ((==@#@$$) :: a6989586621679557194 -> TyFun a6989586621679557194 Bool -> *) 
Instance details
type Apply ((==@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) 
Instance details
type Apply ((==@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 == l2

type (==@#@$$$) (t :: a6989586621679557194) (t1 :: a6989586621679557194) = t == t1 #

type family (x :: a) == (y :: a) :: Bool #

Instances
type (a :: Bool) == (b :: Bool) 
Instance details
type (a :: Bool) == (b :: Bool) = Equals_6989586621679558090 a b
type (a :: Ordering) == (b :: Ordering) 
Instance details
type (a :: Ordering) == (b :: Ordering) = Equals_6989586621679558094 a b
type (a :: Nat) == (b :: Nat) 
Instance details
type (a :: Nat) == (b :: Nat) = a == b
type (a :: Symbol) == (b :: Symbol) 
Instance details
type (a :: Symbol) == (b :: Symbol) = a == b
type (a :: ()) == (b :: ()) 
Instance details
type (a :: ()) == (b :: ()) = Equals_6989586621679558098 a b
type (a :: Void) == (b :: Void) 
Instance details
type (a :: Void) == (b :: Void) = Equals_6989586621679557873 a b
type (a :: Nat) == (b :: Nat) 
Instance details
type (a :: Nat) == (b :: Nat) = Equals_6989586621679059196 a b
type (a2 :: [a1]) == (b :: [a1]) 
Instance details
type (a2 :: [a1]) == (b :: [a1]) = Equals_6989586621679557819 a2 b
type (a2 :: Maybe a1) == (b :: Maybe a1) 
Instance details
type (a2 :: Maybe a1) == (b :: Maybe a1) = Equals_6989586621679557806 a2 b
type (a2 :: NonEmpty a1) == (b :: NonEmpty a1) 
Instance details
type (a2 :: NonEmpty a1) == (b :: NonEmpty a1) = Equals_6989586621679557858 a2 b
type (a2 :: Either a1 b1) == (b2 :: Either a1 b1) 
Instance details
type (a2 :: Either a1 b1) == (b2 :: Either a1 b1) = Equals_6989586621679557839 a2 b2
type (a2 :: (a1, b1)) == (b2 :: (a1, b1)) 
Instance details
type (a2 :: (a1, b1)) == (b2 :: (a1, b1)) = Equals_6989586621679557879 a2 b2
type (a2 :: (a1, b1, c)) == (b2 :: (a1, b1, c)) 
Instance details
type (a2 :: (a1, b1, c)) == (b2 :: (a1, b1, c)) = Equals_6989586621679557898 a2 b2
type (a2 :: (a1, b1, c, d)) == (b2 :: (a1, b1, c, d)) 
Instance details
type (a2 :: (a1, b1, c, d)) == (b2 :: (a1, b1, c, d)) = Equals_6989586621679557924 a2 b2
type (a2 :: (a1, b1, c, d, e)) == (b2 :: (a1, b1, c, d, e)) 
Instance details
type (a2 :: (a1, b1, c, d, e)) == (b2 :: (a1, b1, c, d, e)) = Equals_6989586621679557957 a2 b2
type (a2 :: (a1, b1, c, d, e, f)) == (b2 :: (a1, b1, c, d, e, f)) 
Instance details
type (a2 :: (a1, b1, c, d, e, f)) == (b2 :: (a1, b1, c, d, e, f)) = Equals_6989586621679557997 a2 b2
type (a2 :: (a1, b1, c, d, e, f, g)) == (b2 :: (a1, b1, c, d, e, f, g)) 
Instance details
type (a2 :: (a1, b1, c, d, e, f, g)) == (b2 :: (a1, b1, c, d, e, f, g)) = Equals_6989586621679558044 a2 b2

type family (x :: a) /= (y :: a) :: Bool #

Instances
type (x :: Bool) /= (y :: Bool) 
Instance details
type (x :: Bool) /= (y :: Bool) = Not (x == y)
type (x :: Ordering) /= (y :: Ordering) 
Instance details
type (x :: Ordering) /= (y :: Ordering) = Not (x == y)
type (x :: Nat) /= (y :: Nat) 
Instance details
type (x :: Nat) /= (y :: Nat) = Not (x == y)
type (x :: Symbol) /= (y :: Symbol) 
Instance details
type (x :: Symbol) /= (y :: Symbol) = Not (x == y)
type (x :: ()) /= (y :: ()) 
Instance details
type (x :: ()) /= (y :: ()) = Not (x == y)
type (x :: Void) /= (y :: Void) 
Instance details
type (x :: Void) /= (y :: Void) = Not (x == y)
type (x :: Nat) /= (y :: Nat) 
Instance details
type (x :: Nat) /= (y :: Nat) = Not (x == y)
type (x :: [a]) /= (y :: [a]) 
Instance details
type (x :: [a]) /= (y :: [a]) = Not (x == y)
type (x :: Maybe a) /= (y :: Maybe a) 
Instance details
type (x :: Maybe a) /= (y :: Maybe a) = Not (x == y)
type (x :: NonEmpty a) /= (y :: NonEmpty a) 
Instance details
type (x :: NonEmpty a) /= (y :: NonEmpty a) = Not (x == y)
type (x :: Either a b) /= (y :: Either a b) 
Instance details
type (x :: Either a b) /= (y :: Either a b) = Not (x == y)
type (x :: (a, b)) /= (y :: (a, b)) 
Instance details
type (x :: (a, b)) /= (y :: (a, b)) = Not (x == y)
type (x :: (a, b, c)) /= (y :: (a, b, c)) 
Instance details
type (x :: (a, b, c)) /= (y :: (a, b, c)) = Not (x == y)
type (x :: (a, b, c, d)) /= (y :: (a, b, c, d)) 
Instance details
type (x :: (a, b, c, d)) /= (y :: (a, b, c, d)) = Not (x == y)
type (x :: (a, b, c, d, e)) /= (y :: (a, b, c, d, e)) 
Instance details
type (x :: (a, b, c, d, e)) /= (y :: (a, b, c, d, e)) = Not (x == y)
type (x :: (a, b, c, d, e, f)) /= (y :: (a, b, c, d, e, f)) 
Instance details
type (x :: (a, b, c, d, e, f)) /= (y :: (a, b, c, d, e, f)) = Not (x == y)
type (x :: (a, b, c, d, e, f, g)) /= (y :: (a, b, c, d, e, f, g)) 
Instance details
type (x :: (a, b, c, d, e, f, g)) /= (y :: (a, b, c, d, e, f, g)) = Not (x == y)

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

(%==) :: SEq k => Sing a -> Sing b -> Sing (a == b) #

type EQSym0 = EQ #

type GTSym0 = GT #

type LTSym0 = LT #

data (*@#@$) (l :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type)) :: forall a6989586621679686791. TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> * #

Instances
SuppressUnusedWarnings ((*@#@$) :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> *) 
Instance details
type Apply ((*@#@$) :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> *) (l :: a6989586621679686791) 
Instance details
type Apply ((*@#@$) :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> *) (l :: a6989586621679686791) = (*@#@$$) l

data (l :: a6989586621679686791) *@#@$$ (l1 :: TyFun a6989586621679686791 a6989586621679686791) :: forall a6989586621679686791. a6989586621679686791 -> TyFun a6989586621679686791 a6989586621679686791 -> * #

Instances
SuppressUnusedWarnings ((*@#@$$) :: a6989586621679686791 -> TyFun a6989586621679686791 a6989586621679686791 -> *) 
Instance details
type Apply ((*@#@$$) l1 :: TyFun a a -> *) (l2 :: a) 
Instance details
type Apply ((*@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 * l2

type (*@#@$$$) (t :: a6989586621679686791) (t1 :: a6989586621679686791) = t * t1 #

data (+@#@$) (l :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type)) :: forall a6989586621679686791. TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> * #

Instances
SuppressUnusedWarnings ((+@#@$) :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> *) 
Instance details
type Apply ((+@#@$) :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> *) (l :: a6989586621679686791) 
Instance details
type Apply ((+@#@$) :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> *) (l :: a6989586621679686791) = (+@#@$$) l

data (l :: a6989586621679686791) +@#@$$ (l1 :: TyFun a6989586621679686791 a6989586621679686791) :: forall a6989586621679686791. a6989586621679686791 -> TyFun a6989586621679686791 a6989586621679686791 -> * #

Instances
SuppressUnusedWarnings ((+@#@$$) :: a6989586621679686791 -> TyFun a6989586621679686791 a6989586621679686791 -> *) 
Instance details
type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a) 
Instance details
type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 + l2

type (+@#@$$$) (t :: a6989586621679686791) (t1 :: a6989586621679686791) = t + t1 #

data (-@#@$) (l :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type)) :: forall a6989586621679686791. TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> * #

Instances
SuppressUnusedWarnings ((-@#@$) :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> *) 
Instance details
type Apply ((-@#@$) :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> *) (l :: a6989586621679686791) 
Instance details
type Apply ((-@#@$) :: TyFun a6989586621679686791 (TyFun a6989586621679686791 a6989586621679686791 -> Type) -> *) (l :: a6989586621679686791) = (-@#@$$) l

data (l :: a6989586621679686791) -@#@$$ (l1 :: TyFun a6989586621679686791 a6989586621679686791) :: forall a6989586621679686791. a6989586621679686791 -> TyFun a6989586621679686791 a6989586621679686791 -> * #

Instances
SuppressUnusedWarnings ((-@#@$$) :: a6989586621679686791 -> TyFun a6989586621679686791 a6989586621679686791 -> *) 
Instance details
type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a) 
Instance details
type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 - l2

type (-@#@$$$) (t :: a6989586621679686791) (t1 :: a6989586621679686791) = t - t1 #

data FromIntegerSym0 (l :: TyFun Nat a6989586621679686791) :: forall a6989586621679686791. TyFun Nat a6989586621679686791 -> * #

Instances
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679686791 -> *) 
Instance details
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) 
Instance details
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) = (FromInteger l :: k2)

type FromIntegerSym1 (t :: Nat) = (FromInteger t :: k) #

class PNum a #

Associated Types

type (arg :: a) + (arg1 :: a) :: a #

type (arg :: a) - (arg1 :: a) :: a #

type (arg :: a) * (arg1 :: a) :: a #

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

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

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

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

Instances
PNum Nat 
Instance details

Associated Types

type arg + arg1 :: a #

type arg - arg1 :: a #

type arg * arg1 :: a #

type Negate arg :: a #

type Abs arg :: a #

type Signum arg :: a #

type FromInteger arg :: a #

PNum Nat 
Instance details

Associated Types

type arg + arg1 :: a #

type arg - arg1 :: a #

type arg * arg1 :: a #

type Negate arg :: a #

type Abs arg :: a #

type Signum arg :: a #

type FromInteger arg :: a #

class SNum a where #

Minimal complete definition

(%+), (%*), sAbs, sSignum, sFromInteger

Methods

(%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((+@#@$) :: TyFun a (TyFun a a -> Type) -> *) t1) t2) #

(%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((-@#@$) :: TyFun a (TyFun a a -> Type) -> *) t1) t2) #

(%*) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((*@#@$) :: TyFun a (TyFun a a -> Type) -> *) t1) t2) #

sNegate :: Sing t -> Sing (Apply (NegateSym0 :: TyFun a a -> *) t) #

sAbs :: Sing t -> Sing (Apply (AbsSym0 :: TyFun a a -> *) t) #

sSignum :: Sing t -> Sing (Apply (SignumSym0 :: TyFun a a -> *) t) #

sFromInteger :: Sing t -> Sing (Apply (FromIntegerSym0 :: TyFun Nat a -> *) t) #

Instances
SNum Nat 
Instance details

Methods

(%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) #

(%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) #

(%*) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2) #

sNegate :: Sing t -> Sing (Apply NegateSym0 t) #

sAbs :: Sing t -> Sing (Apply AbsSym0 t) #

sSignum :: Sing t -> Sing (Apply SignumSym0 t) #

sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #

SNum Nat 
Instance details

Methods

(%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) #

(%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) #

(%*) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2) #

sNegate :: Sing t -> Sing (Apply NegateSym0 t) #

sAbs :: Sing t -> Sing (Apply AbsSym0 t) #

sSignum :: Sing t -> Sing (Apply SignumSym0 t) #

sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #

data (<=@#@$) (l :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type)) :: forall a6989586621679568425. TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> * #

Instances
SuppressUnusedWarnings ((<=@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) 
Instance details
type Apply ((<=@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) (l :: a6989586621679568425) 
Instance details
type Apply ((<=@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) (l :: a6989586621679568425) = (<=@#@$$) l

data (l :: a6989586621679568425) <=@#@$$ (l1 :: TyFun a6989586621679568425 Bool) :: forall a6989586621679568425. a6989586621679568425 -> TyFun a6989586621679568425 Bool -> * #

Instances
SuppressUnusedWarnings ((<=@#@$$) :: a6989586621679568425 -> TyFun a6989586621679568425 Bool -> *) 
Instance details
type Apply ((<=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) 
Instance details
type Apply ((<=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 <= l2

type (<=@#@$$$) (t :: a6989586621679568425) (t1 :: a6989586621679568425) = t <= t1 #

data (<@#@$) (l :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type)) :: forall a6989586621679568425. TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> * #

Instances
SuppressUnusedWarnings ((<@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) 
Instance details
type Apply ((<@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) (l :: a6989586621679568425) 
Instance details
type Apply ((<@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) (l :: a6989586621679568425) = (<@#@$$) l

data (l :: a6989586621679568425) <@#@$$ (l1 :: TyFun a6989586621679568425 Bool) :: forall a6989586621679568425. a6989586621679568425 -> TyFun a6989586621679568425 Bool -> * #

Instances
SuppressUnusedWarnings ((<@#@$$) :: a6989586621679568425 -> TyFun a6989586621679568425 Bool -> *) 
Instance details
type Apply ((<@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) 
Instance details
type Apply ((<@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 < l2

type (<@#@$$$) (t :: a6989586621679568425) (t1 :: a6989586621679568425) = t < t1 #

data (>=@#@$) (l :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type)) :: forall a6989586621679568425. TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> * #

Instances
SuppressUnusedWarnings ((>=@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) 
Instance details
type Apply ((>=@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) (l :: a6989586621679568425) 
Instance details
type Apply ((>=@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) (l :: a6989586621679568425) = (>=@#@$$) l

data (l :: a6989586621679568425) >=@#@$$ (l1 :: TyFun a6989586621679568425 Bool) :: forall a6989586621679568425. a6989586621679568425 -> TyFun a6989586621679568425 Bool -> * #

Instances
SuppressUnusedWarnings ((>=@#@$$) :: a6989586621679568425 -> TyFun a6989586621679568425 Bool -> *) 
Instance details
type Apply ((>=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) 
Instance details
type Apply ((>=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 >= l2

type (>=@#@$$$) (t :: a6989586621679568425) (t1 :: a6989586621679568425) = t >= t1 #

data (>@#@$) (l :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type)) :: forall a6989586621679568425. TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> * #

Instances
SuppressUnusedWarnings ((>@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) 
Instance details
type Apply ((>@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) (l :: a6989586621679568425) 
Instance details
type Apply ((>@#@$) :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Bool -> Type) -> *) (l :: a6989586621679568425) = (>@#@$$) l

data (l :: a6989586621679568425) >@#@$$ (l1 :: TyFun a6989586621679568425 Bool) :: forall a6989586621679568425. a6989586621679568425 -> TyFun a6989586621679568425 Bool -> * #

Instances
SuppressUnusedWarnings ((>@#@$$) :: a6989586621679568425 -> TyFun a6989586621679568425 Bool -> *) 
Instance details
type Apply ((>@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) 
Instance details
type Apply ((>@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 > l2

type (>@#@$$$) (t :: a6989586621679568425) (t1 :: a6989586621679568425) = t > t1 #

data CompareSym0 (l :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Ordering -> Type)) :: forall a6989586621679568425. TyFun a6989586621679568425 (TyFun a6989586621679568425 Ordering -> Type) -> * #

Instances
SuppressUnusedWarnings (CompareSym0 :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Ordering -> Type) -> *) 
Instance details
type Apply (CompareSym0 :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Ordering -> Type) -> *) (l :: a6989586621679568425) 
Instance details
type Apply (CompareSym0 :: TyFun a6989586621679568425 (TyFun a6989586621679568425 Ordering -> Type) -> *) (l :: a6989586621679568425) = CompareSym1 l

data CompareSym1 (l :: a6989586621679568425) (l1 :: TyFun a6989586621679568425 Ordering) :: forall a6989586621679568425. a6989586621679568425 -> TyFun a6989586621679568425 Ordering -> * #

Instances
SuppressUnusedWarnings (CompareSym1 :: a6989586621679568425 -> TyFun a6989586621679568425 Ordering -> *) 
Instance details
type Apply (CompareSym1 l1 :: TyFun a Ordering -> *) (l2 :: a) 
Instance details
type Apply (CompareSym1 l1 :: TyFun a Ordering -> *) (l2 :: a) = Compare l1 l2

type CompareSym2 (t :: a6989586621679568425) (t1 :: a6989586621679568425) = Compare t t1 #

data MaxSym0 (l :: TyFun a6989586621679568425 (TyFun a6989586621679568425 a6989586621679568425 -> Type)) :: forall a6989586621679568425. TyFun a6989586621679568425 (TyFun a6989586621679568425 a6989586621679568425 -> Type) -> * #

Instances
SuppressUnusedWarnings (MaxSym0 :: TyFun a6989586621679568425 (TyFun a6989586621679568425 a6989586621679568425 -> Type) -> *) 
Instance details
type Apply (MaxSym0 :: TyFun a6989586621679568425 (TyFun a6989586621679568425 a6989586621679568425 -> Type) -> *) (l :: a6989586621679568425) 
Instance details
type Apply (MaxSym0 :: TyFun a6989586621679568425 (TyFun a6989586621679568425 a6989586621679568425 -> Type) -> *) (l :: a6989586621679568425) = MaxSym1 l

data MaxSym1 (l :: a6989586621679568425) (l1 :: TyFun a6989586621679568425 a6989586621679568425) :: forall a6989586621679568425. a6989586621679568425 -> TyFun a6989586621679568425 a6989586621679568425 -> * #

Instances
SuppressUnusedWarnings (MaxSym1 :: a6989586621679568425 -> TyFun a6989586621679568425 a6989586621679568425 -> *) 
Instance details
type Apply (MaxSym1 l1 :: TyFun a a -> *) (l2 :: a) 
Instance details
type Apply (MaxSym1 l1 :: TyFun a a -> *) (l2 :: a) = Max l1 l2

type MaxSym2 (t :: a6989586621679568425) (t1 :: a6989586621679568425) = Max t t1 #

data MinSym0 (l :: TyFun a6989586621679568425 (TyFun a6989586621679568425 a6989586621679568425 -> Type)) :: forall a6989586621679568425. TyFun a6989586621679568425 (TyFun a6989586621679568425 a6989586621679568425 -> Type) -> * #

Instances
SuppressUnusedWarnings (MinSym0 :: TyFun a6989586621679568425 (TyFun a6989586621679568425 a6989586621679568425 -> Type) -> *) 
Instance details
type Apply (MinSym0 :: TyFun a6989586621679568425 (TyFun a6989586621679568425 a6989586621679568425 -> Type) -> *) (l :: a6989586621679568425) 
Instance details
type Apply (MinSym0 :: TyFun a6989586621679568425 (TyFun a6989586621679568425 a6989586621679568425 -> Type) -> *) (l :: a6989586621679568425) = MinSym1 l

data MinSym1 (l :: a6989586621679568425) (l1 :: TyFun a6989586621679568425 a6989586621679568425) :: forall a6989586621679568425. a6989586621679568425 -> TyFun a6989586621679568425 a6989586621679568425 -> * #

Instances
SuppressUnusedWarnings (MinSym1 :: a6989586621679568425 -> TyFun a6989586621679568425 a6989586621679568425 -> *) 
Instance details
type Apply (MinSym1 l1 :: TyFun a a -> *) (l2 :: a) 
Instance details
type Apply (MinSym1 l1 :: TyFun a a -> *) (l2 :: a) = Min l1 l2

type MinSym2 (t :: a6989586621679568425) (t1 :: a6989586621679568425) = Min t t1 #

class PEq a => POrd a #

Associated Types

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

type (arg :: a) < (arg1 :: a) :: Bool #

type (arg :: a) <= (arg1 :: a) :: Bool #

type (arg :: a) > (arg1 :: a) :: Bool #

type (arg :: a) >= (arg1 :: a) :: Bool #

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

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

Instances
POrd Bool 
Instance details

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

POrd Ordering 
Instance details

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

POrd () 
Instance details

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

POrd Void 
Instance details

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

POrd Nat 
Instance details

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

POrd [a] 
Instance details

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

POrd (Maybe a) 
Instance details

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

POrd (NonEmpty a) 
Instance details

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

POrd (Either a b) 
Instance details

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

POrd (a, b) 
Instance details

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

POrd (a, b, c) 
Instance details

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

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

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

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

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

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

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

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

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

class SEq a => SOrd a where #

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun a (TyFun a Ordering -> Type) -> *) t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((<@#@$) :: TyFun a (TyFun a Bool -> Type) -> *) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((<=@#@$) :: TyFun a (TyFun a Bool -> Type) -> *) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((>@#@$) :: TyFun a (TyFun a Bool -> Type) -> *) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((>=@#@$) :: TyFun a (TyFun a Bool -> Type) -> *) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (MaxSym0 :: TyFun a (TyFun a a -> Type) -> *) t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (MinSym0 :: TyFun a (TyFun a a -> Type) -> *) t1) t2) #

Instances
SOrd Bool 
Instance details

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

SOrd Ordering 
Instance details

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

SOrd () 
Instance details

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

SOrd Void 
Instance details

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

SOrd Nat 
Instance details

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

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

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

SOrd a => SOrd (Maybe a) 
Instance details

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

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

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

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

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

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

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

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

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

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

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

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

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

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

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

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

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

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

generate :: (ListLike (f a) a, HasOrdinal nat) => Sing n -> (Ordinal n -> a) -> Sized f n a #

sIndex :: (HasOrdinal nat, ListLike (f c) c) => Ordinal n -> Sized f n c -> c #

singleton :: ListLike (f a) a => a -> Sized f 1 a #

unsafeFromList :: ListLike (f a) a => Sing n -> [a] -> Sized f n a #

unsafeFromList' :: (SingI n, ListLike (f a) a) => [a] -> Sized f n a #

zipWithSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) c) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c #

pattern (:<) :: forall (f :: * -> *) (n :: Nat) a. ListLike (f a) a => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) => a -> Sized f n1 a -> Sized f n a #

pattern (:>) :: forall (f :: * -> *) (n :: Nat) a. ListLike (f a) a => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) => Sized f n1 a -> a -> Sized f n a #

pattern NilL :: forall (f :: * -> *) (n :: Nat) a. ListLike (f a) a => n ~ 0 => Sized f n a #

pattern NilR :: forall (f :: * -> *) (n :: Nat) a. (ListLike (f a) a, SingI n) => n ~ 0 => Sized f n a #

type family Zero nat :: nat where ... #

Equations

Zero nat = (FromInteger 0 :: nat) 

pattern Succ :: forall nat (n :: nat). IsPeano nat => forall (n1 :: nat). n ~ Succ n1 => Sing n1 -> Sing n #

pattern Zero :: forall nat (n :: nat). IsPeano nat => n ~ Zero nat => Sing n #

minusCong :: (n :~: m) -> (l :~: k) -> (n - l) :~: (m - k) #

minusCongL :: (n :~: m) -> Sing k -> (n - k) :~: (m - k) #

minusCongR :: Sing k -> (n :~: m) -> (k - n) :~: (k - m) #

multCong :: (n :~: m) -> (l :~: k) -> (n * l) :~: (m * k) #

multCongL :: (n :~: m) -> Sing k -> (n * k) :~: (m * k) #

multCongR :: Sing k -> (n :~: m) -> (k * n) :~: (k * m) #

plusCong :: (n :~: m) -> (n' :~: m') -> (n + n') :~: (m + m') #

plusCongL :: (n :~: m) -> Sing k -> (n + k) :~: (m + k) #

plusCongR :: Sing k -> (n :~: m) -> (k + n) :~: (k + m) #

sOne :: SNum nat => Sing (One nat) #

sZero :: SNum nat => Sing (Zero nat) #

succCong :: (n :~: m) -> S n :~: S m #

(%-.) :: PeanoOrder nat => Sing n -> Sing m -> Sing (n -. m) #

coerceLeqL :: IsPeano nat => (n :~: m) -> Sing l -> IsTrue (n <= l) -> IsTrue (m <= l) #

coerceLeqR :: IsPeano nat => Sing l -> (n :~: m) -> IsTrue (l <= n) -> IsTrue (l <= m) #

minPlusTruncMinus :: PeanoOrder nat => Sing n -> Sing m -> (Min n m + (n -. m)) :~: n #

sFlipOrdering :: Sing t -> Sing (Apply FlipOrderingSym0 t) #

sLeqCong :: (a2 :~: b) -> (c :~: d) -> (a2 <= c) :~: (b <= d) #

sLeqCongL :: (a2 :~: b) -> Sing c -> (a2 <= c) :~: (b <= c) #

sLeqCongR :: Sing a2 -> (b :~: c) -> (a2 <= b) :~: (a2 <= c) #

truncMinusLeq :: PeanoOrder nat => Sing n -> Sing m -> IsTrue ((n -. m) <= n) #

class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind nat) => IsPeano nat where #

Methods

succOneCong :: Succ (Zero nat) :~: One nat #

succInj :: (Succ n :~: Succ m) -> n :~: m #

succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ m) -> n :~: m #

succNonCyclic :: Sing n -> (Succ n :~: Zero nat) -> Void #

induction :: p (Zero nat) -> (forall (n :: nat). Sing n -> p n -> p (S n)) -> Sing k -> p k #

plusMinus :: Sing n -> Sing m -> ((n + m) - m) :~: n #

plusMinus' :: Sing n -> Sing m -> ((n + m) - n) :~: m #

plusZeroL :: Sing n -> (Zero nat + n) :~: n #

plusSuccL :: Sing n -> Sing m -> (S n + m) :~: S (n + m) #

plusZeroR :: Sing n -> (n + Zero nat) :~: n #

plusSuccR :: Sing n -> Sing m -> (n + S m) :~: S (n + m) #

plusComm :: Sing n -> Sing m -> (n + m) :~: (m + n) #

plusAssoc :: Sing n -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l)) #

multZeroL :: Sing n -> (Zero nat * n) :~: Zero nat #

multSuccL :: Sing n -> Sing m -> (S n * m) :~: ((n * m) + m) #

multZeroR :: Sing n -> (n * Zero nat) :~: Zero nat #

multSuccR :: Sing n -> Sing m -> (n * S m) :~: ((n * m) + n) #

multComm :: Sing n -> Sing m -> (n * m) :~: (m * n) #

multOneR :: Sing n -> (n * One nat) :~: n #

multOneL :: Sing n -> (One nat * n) :~: n #

plusMultDistrib :: Sing n -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l)) #

multPlusDistrib :: Sing n -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l)) #

minusNilpotent :: Sing n -> (n - n) :~: Zero nat #

multAssoc :: Sing n -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l)) #

plusEqCancelL :: Sing n -> Sing m -> Sing l -> ((n + m) :~: (n + l)) -> m :~: l #

plusEqCancelR :: Sing n -> Sing m -> Sing l -> ((n + l) :~: (m + l)) -> n :~: m #

succAndPlusOneL :: Sing n -> Succ n :~: (One nat + n) #

succAndPlusOneR :: Sing n -> Succ n :~: (n + One nat) #

predSucc :: Sing n -> Pred (Succ n) :~: n #

zeroOrSucc :: Sing n -> ZeroOrSucc n #

plusEqZeroL :: Sing n -> Sing m -> ((n + m) :~: Zero nat) -> n :~: Zero nat #

plusEqZeroR :: Sing n -> Sing m -> ((n + m) :~: Zero nat) -> m :~: Zero nat #

predUnique :: Sing n -> Sing m -> (Succ n :~: m) -> n :~: Pred m #

multEqSuccElimL :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n) #

multEqSuccElimR :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m) #

minusZero :: Sing n -> (n - Zero nat) :~: n #

multEqCancelR :: Sing n -> Sing m -> Sing l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m #

succPred :: Sing n -> ((n :~: Zero nat) -> Void) -> Succ (Pred n) :~: n #

multEqCancelL :: Sing n -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l #

sPred' :: proxy n -> Sing (Succ n) -> Sing n #

toNatural :: Sing n -> Natural #

type family One nat :: nat where ... #

Equations

One nat = (FromInteger 1 :: nat) 

type S (n :: k) = Succ n #

data ZeroOrSucc (n :: nat) :: forall nat. nat -> * where #

Constructors

IsZero :: ZeroOrSucc (Zero nat) 
IsSucc :: ZeroOrSucc (Succ n1) 

type (-.) (n :: k) (m :: k) = Subt n m (m <= n) #

data DiffNat (n :: k) (m :: k) :: forall k. k -> k -> * where #

Constructors

DiffNat :: DiffNat n (n + m1) 

type family FlipOrdering (a :: Ordering) :: Ordering where ... #

data LeqView (n :: nat) (m :: nat) :: forall nat. nat -> nat -> * where #

Constructors

LeqZero :: LeqView (Zero nat) m 
LeqSucc :: LeqView (Succ n1) (Succ m1) 

class (SOrd nat, IsPeano nat) => PeanoOrder nat where #

Methods

leqToCmp :: Sing a -> Sing b -> IsTrue (a <= b) -> Either (a :~: b) (Compare a b :~: LT) #

eqlCmpEQ :: Sing a -> Sing b -> (a :~: b) -> Compare a b :~: EQ #

eqToRefl :: Sing a -> Sing b -> (Compare a b :~: EQ) -> a :~: b #

flipCompare :: Sing a -> Sing b -> FlipOrdering (Compare a b) :~: Compare b a #

ltToNeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> (a :~: b) -> Void #

leqNeqToLT :: Sing a -> Sing b -> IsTrue (a <= b) -> ((a :~: b) -> Void) -> Compare a b :~: LT #

succLeqToLT :: Sing a -> Sing b -> IsTrue (S a <= b) -> Compare a b :~: LT #

ltToLeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> IsTrue (a <= b) #

gtToLeq :: Sing a -> Sing b -> (Compare a b :~: GT) -> IsTrue (b <= a) #

ltToSuccLeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> IsTrue (Succ a <= b) #

cmpZero :: Sing a -> Compare (Zero nat) (Succ a) :~: LT #

leqToGT :: Sing a -> Sing b -> IsTrue (Succ b <= a) -> Compare a b :~: GT #

cmpZero' :: Sing a -> Either (Compare (Zero nat) a :~: EQ) (Compare (Zero nat) a :~: LT) #

zeroNoLT :: Sing a -> (Compare a (Zero nat) :~: LT) -> Void #

ltRightPredSucc :: Sing a -> Sing b -> (Compare a b :~: LT) -> b :~: Succ (Pred b) #

cmpSucc :: Sing n -> Sing m -> Compare n m :~: Compare (Succ n) (Succ m) #

ltSucc :: Sing a -> Compare a (Succ a) :~: LT #

cmpSuccStepR :: Sing n -> Sing m -> (Compare n m :~: LT) -> Compare n (Succ m) :~: LT #

ltSuccLToLT :: Sing n -> Sing m -> (Compare (Succ n) m :~: LT) -> Compare n m :~: LT #

leqToLT :: Sing a -> Sing b -> IsTrue (Succ a <= b) -> Compare a b :~: LT #

leqZero :: Sing n -> IsTrue (Zero nat <= n) #

leqSucc :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (Succ n <= Succ m) #

fromLeqView :: LeqView n m -> IsTrue (n <= m) #

leqViewRefl :: Sing n -> LeqView n n #

viewLeq :: Sing n -> Sing m -> IsTrue (n <= m) -> LeqView n m #

leqWitness :: Sing n -> Sing m -> IsTrue (n <= m) -> DiffNat n m #

leqStep :: Sing n -> Sing m -> Sing l -> ((n + l) :~: m) -> IsTrue (n <= m) #

leqNeqToSuccLeq :: Sing n -> Sing m -> IsTrue (n <= m) -> ((n :~: m) -> Void) -> IsTrue (Succ n <= m) #

leqRefl :: Sing n -> IsTrue (n <= n) #

leqSuccStepR :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (n <= Succ m) #

leqSuccStepL :: Sing n -> Sing m -> IsTrue (Succ n <= m) -> IsTrue (n <= m) #

leqReflexive :: Sing n -> Sing m -> (n :~: m) -> IsTrue (n <= m) #

leqTrans :: Sing n -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue (m <= l) -> IsTrue (n <= l) #

leqAntisymm :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (m <= n) -> n :~: m #

plusMonotone :: Sing n -> Sing m -> Sing l -> Sing k -> IsTrue (n <= m) -> IsTrue (l <= k) -> IsTrue ((n + l) <= (m + k)) #

leqZeroElim :: Sing n -> IsTrue (n <= Zero nat) -> n :~: Zero nat #

plusMonotoneL :: Sing n -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue ((n + l) <= (m + l)) #

plusMonotoneR :: Sing n -> Sing m -> Sing l -> IsTrue (m <= l) -> IsTrue ((n + m) <= (n + l)) #

plusLeqL :: Sing n -> Sing m -> IsTrue (n <= (n + m)) #

plusLeqR :: Sing n -> Sing m -> IsTrue (m <= (n + m)) #

plusCancelLeqR :: Sing n -> Sing m -> Sing l -> IsTrue ((n + l) <= (m + l)) -> IsTrue (n <= m) #

plusCancelLeqL :: Sing n -> Sing m -> Sing l -> IsTrue ((n + m) <= (n + l)) -> IsTrue (m <= l) #

succLeqZeroAbsurd :: Sing n -> IsTrue (S n <= Zero nat) -> Void #

succLeqZeroAbsurd' :: Sing n -> (S n <= Zero nat) :~: False #

succLeqAbsurd :: Sing n -> IsTrue (S n <= n) -> Void #

succLeqAbsurd' :: Sing n -> (S n <= n) :~: False #

notLeqToLeq :: (n <= m) ~ False => Sing n -> Sing m -> IsTrue (m <= n) #

leqSucc' :: Sing n -> Sing m -> (n <= m) :~: (Succ n <= Succ m) #

leqToMin :: Sing n -> Sing m -> IsTrue (n <= m) -> Min n m :~: n #

geqToMin :: Sing n -> Sing m -> IsTrue (m <= n) -> Min n m :~: m #

minComm :: Sing n -> Sing m -> Min n m :~: Min m n #

minLeqL :: Sing n -> Sing m -> IsTrue (Min n m <= n) #

minLeqR :: Sing n -> Sing m -> IsTrue (Min n m <= m) #

minLargest :: Sing l -> Sing n -> Sing m -> IsTrue (l <= n) -> IsTrue (l <= m) -> IsTrue (l <= Min n m) #

leqToMax :: Sing n -> Sing m -> IsTrue (n <= m) -> Max n m :~: m #

geqToMax :: Sing n -> Sing m -> IsTrue (m <= n) -> Max n m :~: n #

maxComm :: Sing n -> Sing m -> Max n m :~: Max m n #

maxLeqR :: Sing n -> Sing m -> IsTrue (m <= Max n m) #

maxLeqL :: Sing n -> Sing m -> IsTrue (n <= Max n m) #

maxLeast :: Sing l -> Sing n -> Sing m -> IsTrue (n <= l) -> IsTrue (m <= l) -> IsTrue (Max n m <= l) #

leqReversed :: Sing n -> Sing m -> (n <= m) :~: (m >= n) #

lneqSuccLeq :: Sing n -> Sing m -> (n < m) :~: (Succ n <= m) #

lneqReversed :: Sing n -> Sing m -> (n < m) :~: (m > n) #

lneqToLT :: Sing n -> Sing m -> IsTrue (n < m) -> Compare n m :~: LT #

ltToLneq :: Sing n -> Sing m -> (Compare n m :~: LT) -> IsTrue (n < m) #

lneqZero :: Sing a -> IsTrue (Zero nat < Succ a) #

lneqSucc :: Sing n -> IsTrue (n < Succ n) #

succLneqSucc :: Sing n -> Sing m -> (n < m) :~: (Succ n < Succ m) #

lneqRightPredSucc :: Sing n -> Sing m -> IsTrue (n < m) -> m :~: Succ (Pred m) #

lneqSuccStepL :: Sing n -> Sing m -> IsTrue (Succ n < m) -> IsTrue (n < m) #

lneqSuccStepR :: Sing n -> Sing m -> IsTrue (n < m) -> IsTrue (n < Succ m) #

plusStrictMonotone :: Sing n -> Sing m -> Sing l -> Sing k -> IsTrue (n < m) -> IsTrue (l < k) -> IsTrue ((n + l) < (m + k)) #

maxZeroL :: Sing n -> Max (Zero nat) n :~: n #

maxZeroR :: Sing n -> Max n (Zero nat) :~: n #

minZeroL :: Sing n -> Min (Zero nat) n :~: Zero nat #

minZeroR :: Sing n -> Min n (Zero nat) :~: Zero nat #

minusSucc :: Sing n -> Sing m -> IsTrue (m <= n) -> (Succ n - m) :~: Succ (n - m) #

lneqZeroAbsurd :: Sing n -> IsTrue (n < Zero nat) -> Void #

minusPlus :: PeanoOrder nat => Sing n -> Sing m -> IsTrue (m <= n) -> ((n - m) + m) :~: n #

(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z #

(=~=) :: r x y -> Sing y -> r x y #

because :: Sing y -> eq x y -> Reason eq x y #

coerce :: (a :=: b) -> f a -> f b #

start :: Preorder eq => Sing a -> eq a a #

withWitness :: IsTrue b -> ((b ~ True) -> r) -> r #

data IsTrue (b :: Bool) where #

Constructors

Witness :: IsTrue True 
Instances
Eq (IsTrue b) 
Instance details

Methods

(==) :: IsTrue b -> IsTrue b -> Bool #

(/=) :: IsTrue b -> IsTrue b -> Bool #

Data (IsTrue True) 
Instance details

Methods

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

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

toConstr :: IsTrue True -> Constr #

dataTypeOf :: IsTrue True -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord (IsTrue b) 
Instance details

Methods

compare :: IsTrue b -> IsTrue b -> Ordering #

(<) :: IsTrue b ->