type-natural-0.7.1.2: 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.Class.Order, Data.Type.Natural.Class
:*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.Class.Order, Data.Type.Natural.Class
:-:Data.Type.Natural
:<=Data.Type.Natural
@+ 
1 (Function)Data.Type.Ordinal
2 (Function)Data.Type.Ordinal.Builtin
3 (Function)Data.Type.Ordinal.Peano
@@Data.Type.Natural
absurdOrd 
1 (Function)Data.Type.Ordinal
2 (Function)Data.Type.Ordinal.Builtin
3 (Function)Data.Type.Ordinal.Peano
ApplyData.Type.Natural
applySingData.Type.Natural
boolToClassLeqData.Type.Natural
boolToPropLeqData.Type.Natural
cmpSuccData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
cmpSuccStepRData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
cmpZeroData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
cmpZero'Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
coerceLeqLData.Type.Natural.Class.Order, Data.Type.Natural.Class
coerceLeqRData.Type.Natural.Class.Order, Data.Type.Natural.Class
DemoteData.Type.Natural
DemoteRepData.Type.Natural
DiffNat 
1 (Type/Class)Data.Type.Natural.Class.Order, Data.Type.Natural.Class
2 (Data Constructor)Data.Type.Natural.Class.Order, Data.Type.Natural.Class
EightData.Type.Natural
eightData.Type.Natural
EighteenData.Type.Natural
eighteenData.Type.Natural
EighteenSym0Data.Type.Natural
EightSym0Data.Type.Natural
ElevenData.Type.Natural
elevenData.Type.Natural
ElevenSym0Data.Type.Natural
enumOrdinal 
1 (Function)Data.Type.Ordinal
2 (Function)Data.Type.Ordinal.Builtin
3 (Function)Data.Type.Ordinal.Peano
eqlCmpEQData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
eqToReflData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
FifteenData.Type.Natural
fifteenData.Type.Natural
FifteenSym0Data.Type.Natural
FiveData.Type.Natural
fiveData.Type.Natural
FiveSym0Data.Type.Natural
flipCompareData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
FlipOrderingData.Type.Natural.Class.Order, Data.Type.Natural.Class
FourData.Type.Natural
fourData.Type.Natural
FourSym0Data.Type.Natural
FourteenData.Type.Natural
fourteenData.Type.Natural
FourteenSym0Data.Type.Natural
fromLeqViewData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
FromPeanoData.Type.Natural.Builtin
fromPeanoInjectiveData.Type.Natural.Builtin
fromPeanoMonotoneData.Type.Natural.Builtin
fromPeanoMultCongData.Type.Natural.Builtin
fromPeanoOneCongData.Type.Natural.Builtin
fromPeanoPlusCongData.Type.Natural.Builtin
fromPeanoSuccCongData.Type.Natural.Builtin
fromPeanoZeroCongData.Type.Natural.Builtin
fromSingData.Type.Natural
fromToPeanoData.Type.Natural.Builtin
geqToMaxData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
geqToMinData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
gtToLeqData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
HasOrdinalData.Type.Ordinal
inclusion 
1 (Function)Data.Type.Ordinal
2 (Function)Data.Type.Ordinal.Builtin
3 (Function)Data.Type.Ordinal.Peano
inclusion' 
1 (Function)Data.Type.Ordinal
2 (Function)Data.Type.Ordinal.Builtin
3 (Function)Data.Type.Ordinal.Peano
inductionData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
inductionNatData.Type.Natural.Builtin
intToNatData.Type.Natural
IsPeanoData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
IsSuccData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
IsZeroData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
KindOfData.Type.Natural
LeqData.Type.Natural
leqAntisymmData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
LeqInstanceData.Type.Natural
leqNeqToLTData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqNeqToSuccLeqData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqReflData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqReflexiveData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqReversedData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqStepData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
LeqSuccData.Type.Natural.Class.Order, Data.Type.Natural.Class
leqSuccData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqSucc'Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqSuccStepLData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqSuccStepRData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqToCmpData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqToGTData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqToLTData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqToMaxData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqToMinData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqTransData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
LeqViewData.Type.Natural.Class.Order, Data.Type.Natural.Class
leqViewReflData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqWitnessData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
LeqZeroData.Type.Natural.Class.Order, Data.Type.Natural.Class
leqZeroData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
leqZeroElimData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
lneqReversedData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
lneqRightPredSuccData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
lneqSuccData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
lneqSuccLeqData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
lneqSuccStepLData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
lneqSuccStepRData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
lneqToLTData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
lneqZeroData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
lneqZeroAbsurdData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
ltRightPredSuccData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
ltSuccData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
ltSuccLToLTData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
ltToLeqData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
ltToLneqData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
ltToNeqData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
ltToSuccLeqData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
MaxData.Type.Natural
maxData.Type.Natural
maxCommData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
maxLeastData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
maxLeqLData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
maxLeqRData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
MaxSym0Data.Type.Natural
MaxSym1Data.Type.Natural
MaxSym2Data.Type.Natural
maxZeroLData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
maxZeroRData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
MinData.Type.Natural
minData.Type.Natural
minCommData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
minLargestData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
minLeqLData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
minLeqRData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
minPlusTruncMinusData.Type.Natural.Class.Order, Data.Type.Natural.Class
MinSym0Data.Type.Natural
MinSym1Data.Type.Natural
MinSym2Data.Type.Natural
minusCongData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
minusCongLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
minusCongRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
minusNilpotentData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
minusPlusData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
minusSuccData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
minusZeroData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
minZeroLData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
minZeroRData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
mkOrdinalQQData.Type.Ordinal
mkSNatQQData.Type.Natural.Class
multAssocData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multCommData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multCongData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural
multCongLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural
multCongRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural
multEqCancelLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multEqCancelRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multEqSuccElimLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multEqSuccElimRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multOneLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multOneRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multPlusDistribData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multSuccLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multSuccRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multZeroLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
multZeroRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
N0Data.Type.Natural
n0Data.Type.Natural
N0Sym0Data.Type.Natural
N1Data.Type.Natural
n1Data.Type.Natural
N10Data.Type.Natural
n10Data.Type.Natural
N10Sym0Data.Type.Natural
N11Data.Type.Natural
n11Data.Type.Natural
N11Sym0Data.Type.Natural
N12Data.Type.Natural
n12Data.Type.Natural
N12Sym0Data.Type.Natural
N13Data.Type.Natural
n13Data.Type.Natural
N13Sym0Data.Type.Natural
N14Data.Type.Natural
n14Data.Type.Natural
N14Sym0Data.Type.Natural
N15Data.Type.Natural
n15Data.Type.Natural
N15Sym0Data.Type.Natural
N16Data.Type.Natural
n16Data.Type.Natural
N16Sym0Data.Type.Natural
N17Data.Type.Natural
n17Data.Type.Natural
N17Sym0Data.Type.Natural
N18Data.Type.Natural
n18Data.Type.Natural
N18Sym0Data.Type.Natural
N19Data.Type.Natural
n19Data.Type.Natural
N19Sym0Data.Type.Natural
N1Sym0Data.Type.Natural
N2Data.Type.Natural
n2Data.Type.Natural
N20Data.Type.Natural
n20Data.Type.Natural
N20Sym0Data.Type.Natural
N2Sym0Data.Type.Natural
N3Data.Type.Natural
n3Data.Type.Natural
N3Sym0Data.Type.Natural
N4Data.Type.Natural
n4Data.Type.Natural
N4Sym0Data.Type.Natural
N5Data.Type.Natural
n5Data.Type.Natural
N5Sym0Data.Type.Natural
N6Data.Type.Natural
n6Data.Type.Natural
N6Sym0Data.Type.Natural
N7Data.Type.Natural
n7Data.Type.Natural
N7Sym0Data.Type.Natural
N8Data.Type.Natural
n8Data.Type.Natural
N8Sym0Data.Type.Natural
N9Data.Type.Natural
n9Data.Type.Natural
N9Sym0Data.Type.Natural
NatData.Type.Natural
natToIntData.Type.Natural
NineData.Type.Natural
nineData.Type.Natural
NineSym0Data.Type.Natural
NineteenData.Type.Natural
nineteenData.Type.Natural
NineteenSym0Data.Type.Natural
nonSLeqToLTData.Type.Natural
notLeqToLeqData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
od 
1 (Function)Data.Type.Ordinal.Builtin
2 (Function)Data.Type.Ordinal.Peano
odLitData.Type.Ordinal
odPNData.Type.Ordinal
OLt 
1 (Data Constructor)Data.Type.Ordinal
2 (Data Constructor)Data.Type.Ordinal.Builtin
3 (Data Constructor)Data.Type.Ordinal.Peano
One 
1 (Type/Class)Data.Type.Natural
2 (Type/Class)Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
oneData.Type.Natural
OneSym0Data.Type.Natural
Ordinal 
1 (Type/Class)Data.Type.Ordinal
2 (Type/Class)Data.Type.Ordinal.Builtin
3 (Type/Class)Data.Type.Ordinal.Peano
ordToInt 
1 (Function)Data.Type.Ordinal
2 (Function)Data.Type.Ordinal.Builtin
3 (Function)Data.Type.Ordinal.Peano
ordToSingData.Type.Ordinal
OS 
1 (Data Constructor)Data.Type.Ordinal
2 (Data Constructor)Data.Type.Ordinal.Builtin
3 (Data Constructor)Data.Type.Ordinal.Peano
OZ 
1 (Data Constructor)Data.Type.Ordinal
2 (Data Constructor)Data.Type.Ordinal.Builtin
3 (Data Constructor)Data.Type.Ordinal.Peano
PeanoData.Type.Natural.Builtin
PeanoOrderData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
plusAssocData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusCancelLeqLData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
plusCancelLeqRData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
plusCommData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusCongData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural
plusCongLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural
plusCongRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural
plusEqCancelLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusEqCancelRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusEqZeroLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusEqZeroRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusInjectiveLData.Type.Natural
plusInjectiveRData.Type.Natural
plusLeqLData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
plusLeqRData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
plusMinusData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusMinus'Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusMinusEqLData.Type.Natural
plusMonotoneData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
plusMonotoneLData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
plusMonotoneRData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
plusMultDistribData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusNeutralLData.Type.Natural
plusNeutralRData.Type.Natural
plusStrictMonotoneData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
plusSuccLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusSuccRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusZeroLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
plusZeroRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
predSuccData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
predUniqueData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
propToBoolLeqData.Type.Natural
propToClassLeqData.Type.Natural
Proxy 
1 (Data Constructor)Data.Type.Natural
2 (Type/Class)Data.Type.Natural
reflToSEqualData.Type.Natural
S 
1 (Data Constructor)Data.Type.Natural
2 (Type/Class)Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
sEightData.Type.Natural
sEighteenData.Type.Natural
sElevenData.Type.Natural
SevenData.Type.Natural
sevenData.Type.Natural
SevenSym0Data.Type.Natural
SeventeenData.Type.Natural
seventeenData.Type.Natural
SeventeenSym0Data.Type.Natural
sFifteenData.Type.Natural
sFiveData.Type.Natural
sFlipOrderingData.Type.Natural.Class.Order, Data.Type.Natural.Class
sFourData.Type.Natural
sFourteenData.Type.Natural
sFromPeanoData.Type.Natural.Builtin
SingData.Type.Natural
singData.Type.Natural
singByProxyData.Type.Natural
singByProxy#Data.Type.Natural
singFun1Data.Type.Natural
singFun2Data.Type.Natural
singFun3Data.Type.Natural
singFun4Data.Type.Natural
singFun5Data.Type.Natural
singFun6Data.Type.Natural
singFun7Data.Type.Natural
singFun8Data.Type.Natural
SingFunction1Data.Type.Natural
SingFunction2Data.Type.Natural
SingFunction3Data.Type.Natural
SingFunction4Data.Type.Natural
SingFunction5Data.Type.Natural
SingFunction6Data.Type.Natural
SingFunction7Data.Type.Natural
SingFunction8Data.Type.Natural
SingIData.Type.Natural
SingInstance 
1 (Data Constructor)Data.Type.Natural
2 (Type/Class)Data.Type.Natural
singInstanceData.Type.Natural
SingKindData.Type.Natural
singThatData.Type.Natural
SixData.Type.Natural
sixData.Type.Natural
SixSym0Data.Type.Natural
SixteenData.Type.Natural
sixteenData.Type.Natural
SixteenSym0Data.Type.Natural
SLambdaData.Type.Natural
sLeqCongData.Type.Natural.Class.Order, Data.Type.Natural.Class
sLeqCongLData.Type.Natural.Class.Order, Data.Type.Natural.Class
sLeqCongRData.Type.Natural.Class.Order, Data.Type.Natural.Class
sLeqReflexiveData.Type.Natural
sMaxData.Type.Natural
sMinData.Type.Natural
sN0Data.Type.Natural
sN1Data.Type.Natural
sN10Data.Type.Natural
sN11Data.Type.Natural
sN12Data.Type.Natural
sN13Data.Type.Natural
sN14Data.Type.Natural
sN15Data.Type.Natural
sN16Data.Type.Natural
sN17Data.Type.Natural
sN18Data.Type.Natural
sN19Data.Type.Natural
sN2Data.Type.Natural
sN20Data.Type.Natural
sN3Data.Type.Natural
sN4Data.Type.Natural
sN5Data.Type.Natural
sN6Data.Type.Natural
sN7Data.Type.Natural
sN8Data.Type.Natural
sN9Data.Type.Natural
SNatData.Type.Natural
snat 
1 (Function)Data.Type.Natural
2 (Function)Data.Type.Natural.Builtin
sNatToIntData.Type.Natural
sNatToOrd 
1 (Function)Data.Type.Ordinal
2 (Function)Data.Type.Ordinal.Builtin
3 (Function)Data.Type.Ordinal.Peano
sNatToOrd' 
1 (Function)Data.Type.Ordinal
2 (Function)Data.Type.Ordinal.Builtin
3 (Function)Data.Type.Ordinal.Peano
snEqZAbsurdData.Type.Natural
sNineData.Type.Natural
sNineteenData.Type.Natural
SomeSing 
1 (Data Constructor)Data.Type.Natural
2 (Type/Class)Data.Type.Natural
sOne 
1 (Function)Data.Type.Natural
2 (Function)Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
sPred'Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
SSData.Type.Natural
sSevenData.Type.Natural
sSeventeenData.Type.Natural
sSixData.Type.Natural
sSixteenData.Type.Natural
SSym0Data.Type.Natural
SSym1Data.Type.Natural
sTenData.Type.Natural
sThirteenData.Type.Natural
sThreeData.Type.Natural
sToPeanoData.Type.Natural.Builtin
sTwelveData.Type.Natural
sTwentyData.Type.Natural
sTwoData.Type.Natural
SuccData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
succAndPlusOneLData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
succAndPlusOneRData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
succCongData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
succInjData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
succInj'Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
succLeqAbsurdData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
succLeqAbsurd'Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
SuccLeqSuccData.Type.Natural
succLeqToLTData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
succLeqZeroAbsurdData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
succLeqZeroAbsurd'Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
succLneqSuccData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
succNonCyclicData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
succOneCongData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
succPredData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
SZData.Type.Natural
sZero 
1 (Function)Data.Type.Natural
2 (Function)Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
TenData.Type.Natural
tenData.Type.Natural
TenSym0Data.Type.Natural
ThirteenData.Type.Natural
thirteenData.Type.Natural
ThirteenSym0Data.Type.Natural
ThreeData.Type.Natural
threeData.Type.Natural
ThreeSym0Data.Type.Natural
toFromPeanoData.Type.Natural.Builtin
ToPeanoData.Type.Natural.Builtin
toPeanoInjectiveData.Type.Natural.Builtin
toPeanoMonotoneData.Type.Natural.Builtin
toPeanoMultCongData.Type.Natural.Builtin
toPeanoOneCongData.Type.Natural.Builtin
toPeanoPlusCongData.Type.Natural.Builtin
toPeanoSuccCongData.Type.Natural.Builtin
toPeanoZeroCongData.Type.Natural.Builtin
toSingData.Type.Natural
truncMinusLeqData.Type.Natural.Class.Order, Data.Type.Natural.Class
TwelveData.Type.Natural
twelveData.Type.Natural
TwelveSym0Data.Type.Natural
TwentyData.Type.Natural
twentyData.Type.Natural
TwentySym0Data.Type.Natural
TwoData.Type.Natural
twoData.Type.Natural
TwoSym0Data.Type.Natural
TyCon1Data.Type.Natural
TyCon2Data.Type.Natural
TyCon3Data.Type.Natural
TyCon4Data.Type.Natural
TyCon5Data.Type.Natural
TyCon6Data.Type.Natural
TyCon7Data.Type.Natural
TyCon8Data.Type.Natural
TyFunData.Type.Natural
unsafeFromInt 
1 (Function)Data.Type.Ordinal
2 (Function)Data.Type.Ordinal.Builtin
3 (Function)Data.Type.Ordinal.Peano
unSingFun1Data.Type.Natural
unSingFun2Data.Type.Natural
unSingFun3Data.Type.Natural
unSingFun4Data.Type.Natural
unSingFun5Data.Type.Natural
unSingFun6Data.Type.Natural
unSingFun7Data.Type.Natural
unSingFun8Data.Type.Natural
vacuousOrd 
1 (Function)Data.Type.Ordinal
2 (Function)Data.Type.Ordinal.Builtin
3 (Function)Data.Type.Ordinal.Peano
viewLeqData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
withSingData.Type.Natural
withSingIData.Type.Natural
withSomeSingData.Type.Natural
ZData.Type.Natural
Zero 
1 (Type/Class)Data.Type.Natural
2 (Type/Class)Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
3 (Data Constructor)Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
zeroData.Type.Natural
ZeroLeqData.Type.Natural
zeroNoLTData.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural
ZeroOrSuccData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class
zeroOrSuccData.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin
ZeroSym0Data.Type.Natural
ZSym0Data.Type.Natural
~>Data.Type.Natural