The module `GHC.TypeLits` provides two views on values of type `TNat`, which make it possible to define inductive functions using `TNat` values.

## Checking for Zero (Unary Strucutre of Nat)

The first view provides the same functionality as the usual Peano arithmetic definition of the natural numbers. It is useful when using `TNat` to count something.

```isZero :: Sing n -> IsZero n

data IsZero :: Nat -> * where
IsZero ::              IsZero 0
IsSucc :: !(Sing n) -> IsZero (n + 1)
```

By using `isZero` we can check if a number is 0 or the successor of another number. The interesting aspect of `isZero` is that the result is typed: if `isZero x` returns `IsSucc y`, then the type checker knows that the type of `y` is one smaller than `x`.

## Checking for Evenness (Binary Structure of Nat)

The other view provides a more "bit-oriented" view of the natural numbers, by allowing us to check if the least significant bit of a number is 0 or 1. It is useful when we use `TNat` values for splitting things in half:

```isEven :: Sing n -> IsEven n

data IsEven a :: Nat -> * where
IsEvenZero ::                  IsEven 0
IsEven     :: !(Sing (n+1)) -> IsEven (2 * n + 2)
IsOdd      :: !(Sing n)     -> IsEven (2 * n + 1)
```