Index
| * | Data.Nat |
| + | Data.Nat |
| - | Data.Nat |
| Cmp | Data.Nat |
| cmp | Data.Nat |
| Compare | Data.Nat |
| Fin | Data.Fin |
| finToInt | Data.Fin |
| finToNat | Data.Fin |
| finZAbsurd | Data.Fin |
| finZElim | Data.Fin |
| FromKnownNat | Data.Nat |
| fromKnownNat | Data.Nat |
| IsNat | Data.Nat |
| IsZero | Data.Nat |
| isZero | Data.Nat |
| last | Data.Fin |
| LTE | Data.Nat |
| lte | Data.Nat |
| Max | Data.Nat |
| maximum | Data.Nat |
| Min | Data.Nat |
| minimum | Data.Nat |
| monus | Data.Nat |
| Nat | Data.Nat |
| natToFin | Data.Fin |
| natToInt | Data.Nat |
| plus | Data.Nat |
| power | Data.Nat |
| Pred | Data.Nat |
| pred | Data.Nat |
| S | Data.Nat |
| SEQ | Data.Nat |
| SGT | Data.Nat |
| shift | Data.Fin |
| SIsZ | Data.Nat |
| SLT | Data.Nat |
| SLTE | Data.Nat |
| SNat | Data.Nat |
| strengthen | Data.Fin |
| succ | |
| 1 (Function) | Data.Nat |
| 2 (Function) | Data.Fin |
| times | Data.Nat |
| ToKnownNat | Data.Nat |
| weaken | Data.Fin |
| weakenLTE | Data.Fin |
| weakenN | Data.Fin |
| witness | Data.Nat |
| Z | Data.Nat |
| zero | |
| 1 (Function) | Data.Nat |
| 2 (Function) | Data.Fin |
| ^ | Data.Nat |