Index
| absurd | Data.Fin |
| append | Data.Fin |
| boring | Data.Fin |
| cata | |
| 1 (Function) | Data.Nat, Data.Type.Nat |
| 2 (Function) | Data.Fin |
| 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 |
| 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 |
| 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 |
| 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 |
| unfoldedFix | Data.Type.Nat |
| universe | Data.Fin |
| universe1 | Data.Fin |
| weakenLeft | Data.Fin |
| weakenRight | Data.Fin |
| Z | |
| 1 (Data Constructor) | Data.Nat, Data.Type.Nat |
| 2 (Data Constructor) | Data.Fin |