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

Index

absurd Data.Fin
append Data.Fin
boring Data.Fin
cata
1 (Function) Data.Nat , Data.Type.Nat
2 (Function) Data.Fin
decideLE
1 (Function) Data.Type.Nat.LE
2 (Function) Data.Type.Nat.LE.ReflStep
discreteNat Data.Type.Nat
DivMod2 Data.Type.Nat
Enum Data.Fin.Enum
EnumSize Data.Fin.Enum
EqNat Data.Type.Nat
eqNat Data.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
Fin Data.Fin
fin0 Data.Fin
fin1 Data.Fin
fin2 Data.Fin
fin3 Data.Fin
fin4 Data.Fin
fin5 Data.Fin
fin6 Data.Fin
fin7 Data.Fin
fin8 Data.Fin
fin9 Data.Fin
from Data.Fin.Enum
FromGHC Data.Type.Nat
fromNat Data.Fin
fromNatural Data.Nat , Data.Type.Nat
fromZeroSucc Data.Type.Nat.LE.ReflStep
FS Data.Fin
FZ Data.Fin
GEnumSize Data.Fin.Enum
GFrom Data.Fin.Enum
gfrom Data.Fin.Enum
GTo Data.Fin.Enum
gto Data.Fin.Enum
induction Data.Type.Nat
induction1 Data.Type.Nat
InlineInduction Data.Type.Nat
inlineInduction Data.Type.Nat
inlineInduction1 Data.Type.Nat
inlineUniverse Data.Fin
inlineUniverse1 Data.Fin
inverse Data.Fin
isMax Data.Fin
isMin Data.Fin
LE Data.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
leProof Data.Type.Nat.LE
LERefl Data.Type.Nat.LE.ReflStep
leRefl
1 (Function) Data.Type.Nat.LE
2 (Function) Data.Type.Nat.LE.ReflStep
LEStep Data.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
LESucc Data.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
LEZero Data.Type.Nat.LE
leZero
1 (Function) Data.Type.Nat.LE
2 (Function) Data.Type.Nat.LE.ReflStep
LT Data.Type.Nat.LT
LTProof Data.Type.Nat.LT
ltProof Data.Type.Nat.LT
ltReflAbsurd Data.Type.Nat.LT
ltSymAbsurd Data.Type.Nat.LT
ltTrans Data.Type.Nat.LT
mirror Data.Fin
Mult Data.Type.Nat
Mult2 Data.Type.Nat
Nat Data.Nat , Data.Type.Nat
Nat0 Data.Type.Nat
nat0 Data.Nat , Data.Type.Nat
Nat1 Data.Type.Nat
nat1 Data.Nat , Data.Type.Nat
Nat2 Data.Type.Nat
nat2 Data.Nat , Data.Type.Nat
Nat3 Data.Type.Nat
nat3 Data.Nat , Data.Type.Nat
Nat4 Data.Type.Nat
nat4 Data.Nat , Data.Type.Nat
Nat5 Data.Type.Nat
nat5 Data.Nat , Data.Type.Nat
Nat6 Data.Type.Nat
nat6 Data.Nat , Data.Type.Nat
Nat7 Data.Type.Nat
nat7 Data.Nat , Data.Type.Nat
Nat8 Data.Type.Nat
nat8 Data.Nat , Data.Type.Nat
Nat9 Data.Type.Nat
nat9 Data.Nat , Data.Type.Nat
Plus Data.Type.Nat
proofMultNOne Data.Type.Nat
proofMultNZero Data.Type.Nat
proofMultOneN Data.Type.Nat
proofMultZeroN Data.Type.Nat
proofPlusNZero Data.Type.Nat
proofPlusZeroN Data.Type.Nat
proofZeroLEZero
1 (Function) Data.Type.Nat.LE
2 (Function) Data.Type.Nat.LE.ReflStep
reflect Data.Type.Nat
reflectToNum Data.Type.Nat
reify Data.Type.Nat
S Data.Nat , Data.Type.Nat
SNat Data.Type.Nat
snat Data.Type.Nat
SNatI Data.Type.Nat
snatToNat Data.Type.Nat
snatToNatural Data.Type.Nat
split Data.Fin
SS Data.Type.Nat
SZ Data.Type.Nat
to Data.Fin.Enum
ToGHC Data.Type.Nat
toInteger Data.Fin
toNat Data.Fin
toNatural
1 (Function) Data.Nat , Data.Type.Nat
2 (Function) Data.Fin
toZeroSucc Data.Type.Nat.LE.ReflStep
unfoldedFix Data.Type.Nat
universe Data.Fin
universe1 Data.Fin
weakenLeft Data.Fin
weakenLeft1 Data.Fin
weakenRight Data.Fin
weakenRight1 Data.Fin
withLEProof Data.Type.Nat.LE
withLTProof Data.Type.Nat.LT
withSNat Data.Type.Nat
Z Data.Nat , Data.Type.Nat