Contents
Index
type-natural-0.3.0.0: Type-level natural and proofs of their properties.
Index
%*
Data.Type.Natural
%**
Data.Type.Natural
%+
Data.Type.Natural
%-
Data.Type.Natural
%:*
Data.Type.Natural
%:**
Data.Type.Natural
%:+
Data.Type.Natural
%:-
Data.Type.Natural
%:<<=
Data.Type.Natural
:*
Data.Type.Natural
:*$
Data.Type.Natural
:*$$
Data.Type.Natural
:*$$$
Data.Type.Natural
:**
Data.Type.Natural
:**:
Data.Type.Natural
:*:
Data.Type.Natural
:+
Data.Type.Natural
:+$
Data.Type.Natural
:+$$
Data.Type.Natural
:+$$$
Data.Type.Natural
:+:
Data.Type.Natural
:-
Data.Type.Natural
:-$
Data.Type.Natural
:-$$
Data.Type.Natural
:-$$$
Data.Type.Natural
:-:
Data.Type.Natural
:<<=
Data.Type.Natural
:<<=$
Data.Type.Natural
:<<=$$
Data.Type.Natural
:<<=$$$
Data.Type.Natural
:<=
Data.Type.Natural
@+
Data.Type.Ordinal
@@
Data.Type.Natural
absurdOrd
Data.Type.Ordinal
Apply
Data.Type.Natural
applySing
Data.Type.Natural
boolToClassLeq
Data.Type.Natural
boolToPropLeq
Data.Type.Natural
bugInGHC
Data.Type.Natural
CastedOrdinal
1 (Type/Class)
Data.Type.Ordinal
2 (Data Constructor)
Data.Type.Ordinal
Demote
Data.Type.Natural
DemoteRep
Data.Type.Natural
Eight
Data.Type.Natural
eight
Data.Type.Natural
Eighteen
Data.Type.Natural
eighteen
Data.Type.Natural
EighteenSym0
Data.Type.Natural
EightSym0
Data.Type.Natural
Eleven
Data.Type.Natural
eleven
Data.Type.Natural
ElevenSym0
Data.Type.Natural
enumOrdinal
Data.Type.Ordinal
eqPreservesS
Data.Type.Natural
eqSuccMinus
Data.Type.Natural
Fifteen
Data.Type.Natural
fifteen
Data.Type.Natural
FifteenSym0
Data.Type.Natural
Five
Data.Type.Natural
five
Data.Type.Natural
FiveSym0
Data.Type.Natural
Four
Data.Type.Natural
four
Data.Type.Natural
FourSym0
Data.Type.Natural
Fourteen
Data.Type.Natural
fourteen
Data.Type.Natural
FourteenSym0
Data.Type.Natural
fromSing
Data.Type.Natural
inclusion
Data.Type.Ordinal
inclusion'
Data.Type.Ordinal
intToNat
Data.Type.Natural
KindOf
Data.Type.Natural
KProxy
1 (Data Constructor)
Data.Type.Natural
2 (Type/Class)
Data.Type.Natural
Leq
Data.Type.Natural
leqAnitsymmetric
Data.Type.Natural
LeqInstance
Data.Type.Natural
leqLhs
Data.Type.Natural
leqnZElim
Data.Type.Natural
leqPred
Data.Type.Natural
leqRefl
Data.Type.Natural
leqRhs
Data.Type.Natural
leqSnLeq
Data.Type.Natural
leqSnnAbsurd
Data.Type.Natural
leqSnZAbsurd
Data.Type.Natural
leqSucc
Data.Type.Natural
leqTrans
Data.Type.Natural
LeqTrueInstance
Data.Type.Natural
Max
Data.Type.Natural
max
Data.Type.Natural
maxComm
Data.Type.Natural
maxLeqL
Data.Type.Natural
maxLeqR
Data.Type.Natural
MaxSym0
Data.Type.Natural
MaxSym1
Data.Type.Natural
MaxSym2
Data.Type.Natural
maxZL
Data.Type.Natural
maxZR
Data.Type.Natural
Min
Data.Type.Natural
min
Data.Type.Natural
minComm
Data.Type.Natural
minLeqL
Data.Type.Natural
minLeqR
Data.Type.Natural
MinSym0
Data.Type.Natural
MinSym1
Data.Type.Natural
MinSym2
Data.Type.Natural
minusCongEq
Data.Type.Natural
minusNilpotent
Data.Type.Natural
multAssociative
Data.Type.Natural
multComm
Data.Type.Natural
multCongL
Data.Type.Natural
multCongR
Data.Type.Natural
multOneL
Data.Type.Natural
multOneR
Data.Type.Natural
multPlusDistr
Data.Type.Natural
multZL
Data.Type.Natural
multZR
Data.Type.Natural
N0
Data.Type.Natural
n0
Data.Type.Natural
N0Sym0
Data.Type.Natural
N1
Data.Type.Natural
n1
Data.Type.Natural
N10
Data.Type.Natural
n10
Data.Type.Natural
N10Sym0
Data.Type.Natural
N11
Data.Type.Natural
n11
Data.Type.Natural
N11Sym0
Data.Type.Natural
N12
Data.Type.Natural
n12
Data.Type.Natural
N12Sym0
Data.Type.Natural
N13
Data.Type.Natural
n13
Data.Type.Natural
N13Sym0
Data.Type.Natural
N14
Data.Type.Natural
n14
Data.Type.Natural
N14Sym0
Data.Type.Natural
N15
Data.Type.Natural
n15
Data.Type.Natural
N15Sym0
Data.Type.Natural
N16
Data.Type.Natural
n16
Data.Type.Natural
N16Sym0
Data.Type.Natural
N17
Data.Type.Natural
n17
Data.Type.Natural
N17Sym0
Data.Type.Natural
N18
Data.Type.Natural
n18
Data.Type.Natural
N18Sym0
Data.Type.Natural
N19
Data.Type.Natural
n19
Data.Type.Natural
N19Sym0
Data.Type.Natural
N1Sym0
Data.Type.Natural
N2
Data.Type.Natural
n2
Data.Type.Natural
N20
Data.Type.Natural
n20
Data.Type.Natural
N20Sym0
Data.Type.Natural
N2Sym0
Data.Type.Natural
N3
Data.Type.Natural
n3
Data.Type.Natural
N3Sym0
Data.Type.Natural
N4
Data.Type.Natural
n4
Data.Type.Natural
N4Sym0
Data.Type.Natural
N5
Data.Type.Natural
n5
Data.Type.Natural
N5Sym0
Data.Type.Natural
N6
Data.Type.Natural
n6
Data.Type.Natural
N6Sym0
Data.Type.Natural
N7
Data.Type.Natural
n7
Data.Type.Natural
N7Sym0
Data.Type.Natural
N8
Data.Type.Natural
n8
Data.Type.Natural
N8Sym0
Data.Type.Natural
N9
Data.Type.Natural
n9
Data.Type.Natural
N9Sym0
Data.Type.Natural
Nat
Data.Type.Natural
nat
Data.Type.Natural
natToInt
Data.Type.Natural
Nine
Data.Type.Natural
nine
Data.Type.Natural
NineSym0
Data.Type.Natural
Nineteen
Data.Type.Natural
nineteen
Data.Type.Natural
NineteenSym0
Data.Type.Natural
od
Data.Type.Ordinal
One
Data.Type.Natural
one
Data.Type.Natural
OneSym0
Data.Type.Natural
Ordinal
Data.Type.Ordinal
ordToInt
Data.Type.Ordinal
ordToSNat
Data.Type.Ordinal
ordToSNat'
Data.Type.Ordinal
OS
Data.Type.Ordinal
OZ
Data.Type.Ordinal
plusAssociative
Data.Type.Natural
plusCommutative
Data.Type.Natural
plusCongL
Data.Type.Natural
plusCongR
Data.Type.Natural
plusInjectiveL
Data.Type.Natural
plusInjectiveR
Data.Type.Natural
plusLeqL
Data.Type.Natural
plusLeqR
Data.Type.Natural
plusMinusEqL
Data.Type.Natural
plusMinusEqR
Data.Type.Natural
plusMonotone
Data.Type.Natural
plusMultDistr
Data.Type.Natural
plusNeutralL
Data.Type.Natural
plusNeutralR
Data.Type.Natural
plusSR
Data.Type.Natural
plusZL
Data.Type.Natural
plusZR
Data.Type.Natural
propToBoolLeq
Data.Type.Natural
propToClassLeq
Data.Type.Natural
S
Data.Type.Natural
sAndPlusOne
Data.Type.Natural
sEight
Data.Type.Natural
sEighteen
Data.Type.Natural
sEleven
Data.Type.Natural
Seven
Data.Type.Natural
seven
Data.Type.Natural
SevenSym0
Data.Type.Natural
Seventeen
Data.Type.Natural
seventeen
Data.Type.Natural
SeventeenSym0
Data.Type.Natural
sFifteen
Data.Type.Natural
sFive
Data.Type.Natural
sFour
Data.Type.Natural
sFourteen
Data.Type.Natural
Sing
Data.Type.Natural
sing
Data.Type.Natural
singByProxy
Data.Type.Natural
singByProxy#
Data.Type.Natural
singFun1
Data.Type.Natural
singFun2
Data.Type.Natural
singFun3
Data.Type.Natural
singFun4
Data.Type.Natural
singFun5
Data.Type.Natural
singFun6
Data.Type.Natural
singFun7
Data.Type.Natural
singFun8
Data.Type.Natural
SingFunction1
Data.Type.Natural
SingFunction2
Data.Type.Natural
SingFunction3
Data.Type.Natural
SingFunction4
Data.Type.Natural
SingFunction5
Data.Type.Natural
SingFunction6
Data.Type.Natural
SingFunction7
Data.Type.Natural
SingFunction8
Data.Type.Natural
SingI
Data.Type.Natural
SingInstance
1 (Type/Class)
Data.Type.Natural
2 (Data Constructor)
Data.Type.Natural
singInstance
Data.Type.Natural
SingKind
Data.Type.Natural
singThat
Data.Type.Natural
Six
Data.Type.Natural
six
Data.Type.Natural
SixSym0
Data.Type.Natural
Sixteen
Data.Type.Natural
sixteen
Data.Type.Natural
SixteenSym0
Data.Type.Natural
SLambda
Data.Type.Natural
sMax
Data.Type.Natural
sMin
Data.Type.Natural
sN0
Data.Type.Natural
sN1
Data.Type.Natural
sN10
Data.Type.Natural
sN11
Data.Type.Natural
sN12
Data.Type.Natural
sN13
Data.Type.Natural
sN14
Data.Type.Natural
sN15
Data.Type.Natural
sN16
Data.Type.Natural
sN17
Data.Type.Natural
sN18
Data.Type.Natural
sN19
Data.Type.Natural
sN2
Data.Type.Natural
sN20
Data.Type.Natural
sN3
Data.Type.Natural
sN4
Data.Type.Natural
sN5
Data.Type.Natural
sN6
Data.Type.Natural
sN7
Data.Type.Natural
sN8
Data.Type.Natural
sN9
Data.Type.Natural
SNat
Data.Type.Natural
snat
Data.Type.Natural
sNatToInt
Data.Type.Natural
sNatToOrd
Data.Type.Ordinal
sNatToOrd'
Data.Type.Ordinal
snEqZAbsurd
Data.Type.Natural
sNine
Data.Type.Natural
sNineteen
Data.Type.Natural
SomeSing
1 (Type/Class)
Data.Type.Natural
2 (Data Constructor)
Data.Type.Natural
sOne
Data.Type.Natural
SS
Data.Type.Natural
sS
Data.Type.Natural
sSeven
Data.Type.Natural
sSeventeen
Data.Type.Natural
sSix
Data.Type.Natural
sSixteen
Data.Type.Natural
SSym0
Data.Type.Natural
SSym1
Data.Type.Natural
sTen
Data.Type.Natural
sThirteen
Data.Type.Natural
sThree
Data.Type.Natural
sTwelve
Data.Type.Natural
sTwenty
Data.Type.Natural
sTwo
Data.Type.Natural
succCongEq
Data.Type.Natural
succInjective
Data.Type.Natural
SuccLeqSucc
Data.Type.Natural
succPlusL
Data.Type.Natural
succPlusR
Data.Type.Natural
SZ
Data.Type.Natural
sZ
Data.Type.Natural
sZero
Data.Type.Natural
Ten
Data.Type.Natural
ten
Data.Type.Natural
TenSym0
Data.Type.Natural
Thirteen
Data.Type.Natural
thirteen
Data.Type.Natural
ThirteenSym0
Data.Type.Natural
Three
Data.Type.Natural
three
Data.Type.Natural
ThreeSym0
Data.Type.Natural
toSing
Data.Type.Natural
Twelve
Data.Type.Natural
twelve
Data.Type.Natural
TwelveSym0
Data.Type.Natural
Twenty
Data.Type.Natural
twenty
Data.Type.Natural
TwentySym0
Data.Type.Natural
Two
Data.Type.Natural
two
Data.Type.Natural
TwoSym0
Data.Type.Natural
TyCon1
Data.Type.Natural
TyCon2
Data.Type.Natural
TyCon3
Data.Type.Natural
TyCon4
Data.Type.Natural
TyCon5
Data.Type.Natural
TyCon6
Data.Type.Natural
TyCon7
Data.Type.Natural
TyCon8
Data.Type.Natural
TyFun
Data.Type.Natural
unsafeFromInt
Data.Type.Ordinal
unSingFun1
Data.Type.Natural
unSingFun2
Data.Type.Natural
unSingFun3
Data.Type.Natural
unSingFun4
Data.Type.Natural
unSingFun5
Data.Type.Natural
unSingFun6
Data.Type.Natural
unSingFun7
Data.Type.Natural
unSingFun8
Data.Type.Natural
vacuousOrd
Data.Type.Ordinal
vacuousOrdM
Data.Type.Ordinal
withSing
Data.Type.Natural
withSingI
Data.Type.Natural
withSomeSing
Data.Type.Natural
Z
Data.Type.Natural
zAbsorbsMinL
Data.Type.Natural
zAbsorbsMinR
Data.Type.Natural
Zero
Data.Type.Natural
zero
Data.Type.Natural
ZeroLeq
Data.Type.Natural
ZeroSym0
Data.Type.Natural
ZSym0
Data.Type.Natural