fin-0.2.1: Nat and Fin: peano naturals and finite numbers

Index

absurdData.Fin
appendData.Fin
boringData.Fin
cata 
1 (Function)Data.Nat, Data.Type.Nat
2 (Function)Data.Fin
cmpNatData.Type.Nat
decideLE 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
discreteNatData.Type.Nat
DivMod2Data.Type.Nat
EnumData.Fin.Enum
EnumSizeData.Fin.Enum
EqNatData.Type.Nat
eqNatData.Type.Nat
explicitShow 
1 (Function)Data.Nat, Data.Type.Nat
2 (Function)Data.Fin
explicitShowsPrec 
1 (Function)Data.Nat, Data.Type.Nat
2 (Function)Data.Fin
FinData.Fin
fin0Data.Fin
fin1Data.Fin
fin2Data.Fin
fin3Data.Fin
fin4Data.Fin
fin5Data.Fin
fin6Data.Fin
fin7Data.Fin
fin8Data.Fin
fin9Data.Fin
fromData.Fin.Enum
FromGHCData.Type.Nat
fromNatData.Fin
fromNaturalData.Nat, Data.Type.Nat
fromZeroSuccData.Type.Nat.LE.ReflStep
FSData.Fin
FZData.Fin
GEnumSizeData.Fin.Enum
GFromData.Fin.Enum
gfromData.Fin.Enum
GToData.Fin.Enum
gtoData.Fin.Enum
inductionData.Type.Nat
induction1Data.Type.Nat
inlineUniverseData.Fin
inlineUniverse1Data.Fin
inverseData.Fin
isMaxData.Fin
isMinData.Fin
LEData.Type.Nat.LE
leAsym 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
lePred 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
LEProof 
1 (Type/Class)Data.Type.Nat.LE
2 (Type/Class)Data.Type.Nat.LE.ReflStep
leProofData.Type.Nat.LE
LEReflData.Type.Nat.LE.ReflStep
leRefl 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
LEStepData.Type.Nat.LE.ReflStep
leStep 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
leStepL 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
LESuccData.Type.Nat.LE
leSucc 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
leSwap 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
leSwap' 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
leTrans 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
LEZeroData.Type.Nat.LE
leZero 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
LTData.Type.Nat.LT
LTProofData.Type.Nat.LT
ltProofData.Type.Nat.LT
ltReflAbsurdData.Type.Nat.LT
ltSymAbsurdData.Type.Nat.LT
ltTransData.Type.Nat.LT
mirrorData.Fin
MultData.Type.Nat
Mult2Data.Type.Nat
NatData.Nat, Data.Type.Nat
Nat0Data.Type.Nat
nat0Data.Nat, Data.Type.Nat
Nat1Data.Type.Nat
nat1Data.Nat, Data.Type.Nat
Nat2Data.Type.Nat
nat2Data.Nat, Data.Type.Nat
Nat3Data.Type.Nat
nat3Data.Nat, Data.Type.Nat
Nat4Data.Type.Nat
nat4Data.Nat, Data.Type.Nat
Nat5Data.Type.Nat
nat5Data.Nat, Data.Type.Nat
Nat6Data.Type.Nat
nat6Data.Nat, Data.Type.Nat
Nat7Data.Type.Nat
nat7Data.Nat, Data.Type.Nat
Nat8Data.Type.Nat
nat8Data.Nat, Data.Type.Nat
Nat9Data.Type.Nat
nat9Data.Nat, Data.Type.Nat
PlusData.Type.Nat
proofMultNOneData.Type.Nat
proofMultNZeroData.Type.Nat
proofMultOneNData.Type.Nat
proofMultZeroNData.Type.Nat
proofPlusNZeroData.Type.Nat
proofPlusZeroNData.Type.Nat
proofZeroLEZero 
1 (Function)Data.Type.Nat.LE
2 (Function)Data.Type.Nat.LE.ReflStep
reflectData.Type.Nat
reflectToNumData.Type.Nat
reifyData.Type.Nat
SData.Nat, Data.Type.Nat
SNatData.Type.Nat
snatData.Type.Nat
SNatIData.Type.Nat
snatToNatData.Type.Nat
snatToNaturalData.Type.Nat
splitData.Fin
SSData.Type.Nat
SZData.Type.Nat
toData.Fin.Enum
ToGHCData.Type.Nat
toIntegerData.Fin
toNatData.Fin
toNatural 
1 (Function)Data.Nat, Data.Type.Nat
2 (Function)Data.Fin
toZeroSuccData.Type.Nat.LE.ReflStep
unfoldedFixData.Type.Nat
universeData.Fin
universe1Data.Fin
weakenLeftData.Fin
weakenLeft1Data.Fin
weakenRightData.Fin
weakenRight1Data.Fin
withLEProofData.Type.Nat.LE
withLTProofData.Type.Nat.LT
withSNatData.Type.Nat
ZData.Nat, Data.Type.Nat