/Prelude-v19.0.0/Natural/fold.dhall

Copy path to clipboard

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

Examples

fold 3 Natural (λ(x : Natural) → 5 * x) 1 ≡ 125
  (λ(zero : Natural) → fold 3 Natural (λ(x : Natural) → 5 * x) zero)
≡ (λ(zero : Natural) → 5 * (5 * (5 * zero)))
  ( λ(natural : Type) →
λ(succ : naturalnatural) →
λ(zero : natural) →
fold 3 natural succ zero
)
≡ ( λ(natural : Type) →
λ(succ : naturalnatural) →
λ(zero : natural) →
succ (succ (succ zero))
)

Source

{-|
`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 Natural (λ(x : Natural) → 5 * x) 1 ≡ 125

let example1 =
assert
: (λ(zero : Natural) → fold 3 Natural (λ(x : Natural) → 5 * x) zero)
≡ (λ(zero : Natural) → 5 * (5 * (5 * zero)))

let example2 =
assert
: ( λ(natural : Type) →
λ(succ : naturalnatural) →
λ(zero : natural) →
fold 3 natural succ zero
)
≡ ( λ(natural : Type) →
λ(succ : naturalnatural) →
λ(zero : natural) →
succ (succ (succ zero))
)

in fold