28 lines
759 B
Text
28 lines
759 B
Text
{-|
|
|
`fold` is the primitive function for consuming `Natural` numbers
|
|
|
|
If you treat the number `3` as `succ (succ (succ zero))` then a `fold` just
|
|
replaces each `succ` and `zero` with something else
|
|
-}
|
|
let fold
|
|
: Natural →
|
|
∀(natural : Type) →
|
|
∀(succ : natural → natural) →
|
|
∀(zero : natural) →
|
|
natural
|
|
= Natural/fold
|
|
|
|
let example0 = assert : fold 3 Text (λ(x : Text) → "A" ++ x) "B" ≡ "AAAB"
|
|
|
|
let example1 =
|
|
λ(zero : Text) →
|
|
assert
|
|
: fold 3 Text (λ(x : Text) → "A" ++ x) zero
|
|
≡ "A" ++ ("A" ++ ("A" ++ zero))
|
|
|
|
let example2 =
|
|
λ(succ : Text → Text) →
|
|
λ(zero : Text) →
|
|
assert : fold 3 Text succ zero ≡ succ (succ (succ zero))
|
|
|
|
in fold
|