| 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 |
| 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 |
| 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 |
| 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 |
| Mult | 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 | |
| 1 (Data Constructor) | Data.Nat, Data.Type.Nat |
| 2 (Data Constructor) | Data.Fin |
| 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 |
| weakenRight | Data.Fin |
| withLEProof | Data.Type.Nat.LE |
| withLTProof | Data.Type.Nat.LT |
| withSNat | Data.Type.Nat |
| Z | |
| 1 (Data Constructor) | Data.Nat, Data.Type.Nat |
| 2 (Data Constructor) | Data.Fin |