fin-0: Nat and Fin

Index

absurdData.Fin
boringData.Fin
cata 
1 (Function)Data.Nat, Data.Type.Nat
2 (Function)Data.Fin
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
firstData.Fin
FiveData.Type.Nat
fiveData.Nat, Data.Type.Nat
FourData.Type.Nat
fourData.Nat, Data.Type.Nat
fromNatData.Fin
fromNaturalData.Nat, Data.Type.Nat
inductionData.Type.Nat
induction1Data.Type.Nat
InlineInductionData.Type.Nat
inlineInductionData.Type.Nat
inlineInduction1Data.Type.Nat
inlineUniverseData.Fin
inverseData.Fin
MultData.Type.Nat
NatData.Nat, Data.Type.Nat
OneData.Type.Nat
oneData.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
reflectData.Type.Nat
reflectToNumData.Type.Nat
reifyData.Type.Nat
S 
1 (Data Constructor)Data.Nat, Data.Type.Nat
2 (Data Constructor)Data.Fin
SNatData.Type.Nat
snatData.Type.Nat
SNatIData.Type.Nat
snatToNatData.Type.Nat
snatToNaturalData.Type.Nat
SSData.Type.Nat
SZData.Type.Nat
ThreeData.Type.Nat
threeData.Nat, Data.Type.Nat
toIntegerData.Fin
toNatData.Fin
toNatural 
1 (Function)Data.Nat, Data.Type.Nat
2 (Function)Data.Fin
TwoData.Type.Nat
twoData.Nat, Data.Type.Nat
universeData.Fin
Z 
1 (Data Constructor)Data.Nat, Data.Type.Nat
2 (Data Constructor)Data.Fin
ZeroData.Type.Nat
zeroData.Nat, Data.Type.Nat
zerothData.Fin