... | ... | @@ -22,13 +22,13 @@ 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
|
|
|
then `x`.
|
|
|
than `x`.
|
|
|
|
|
|
## Checking for Evenness (Binary Structure of Nat)
|
|
|
|
|
|
|
|
|
The other view provides a more "bit-oriented" view of
|
|
|
the natural numbers, by allowing is to check if the least
|
|
|
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:
|
... | ... | @@ -37,7 +37,7 @@ in half: |
|
|
isEven :: TNat n -> IsEven n
|
|
|
|
|
|
data IsEven a :: Nat -> * where
|
|
|
IsEvenZero :: IsEven 0
|
|
|
IsEven :: !(TNat (n + 1)) -> IsEven (2 * (n + 1))
|
|
|
IsOdd :: !(TNat n) -> IsEven ((2 * n) + 1)
|
|
|
IsEvenZero :: IsEven 0
|
|
|
IsEven :: !(TNat n) -> IsEven (2 * n + 2)
|
|
|
IsOdd :: !(TNat n) -> IsEven (2 * n + 1)
|
|
|
``` |
|
|
\ No newline at end of file |