Index
| absurd | Data.Fin |
| boring | Data.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 |
| Fin | Data.Fin |
| first | Data.Fin |
| Five | Data.Type.Nat |
| five | Data.Nat, Data.Type.Nat |
| Four | Data.Type.Nat |
| four | Data.Nat, Data.Type.Nat |
| fromNat | Data.Fin |
| fromNatural | Data.Nat, Data.Type.Nat |
| induction | Data.Type.Nat |
| induction1 | Data.Type.Nat |
| InlineInduction | Data.Type.Nat |
| inlineInduction | Data.Type.Nat |
| inlineInduction1 | Data.Type.Nat |
| inlineUniverse | Data.Fin |
| inverse | Data.Fin |
| Mult | Data.Type.Nat |
| Nat | Data.Nat, Data.Type.Nat |
| One | Data.Type.Nat |
| one | 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 |
| SS | Data.Type.Nat |
| SZ | Data.Type.Nat |
| Three | Data.Type.Nat |
| three | Data.Nat, Data.Type.Nat |
| toInteger | Data.Fin |
| toNat | Data.Fin |
| toNatural | |
| 1 (Function) | Data.Nat, Data.Type.Nat |
| 2 (Function) | Data.Fin |
| Two | Data.Type.Nat |
| two | Data.Nat, Data.Type.Nat |
| universe | Data.Fin |
| Z | |
| 1 (Data Constructor) | Data.Nat, Data.Type.Nat |
| 2 (Data Constructor) | Data.Fin |
| Zero | Data.Type.Nat |
| zero | Data.Nat, Data.Type.Nat |
| zeroth | Data.Fin |