/Prelude-v21.1.0/Natural/build.dhall

Copy path to clipboard

build is the inverse of fold

Examples

  build
( λ(natural : Type) →
λ(succ : naturalnatural) →
λ(zero : natural) →
succ (succ (succ zero))
)
≡ 3
  build
(λ(natural : Type) → λ(succ : naturalnatural) → λ(zero : natural) → zero)
≡ 0

Source

--| `build` is the inverse of `fold`
let build
: ( ∀(natural : Type) →
∀(succ : natural → natural) →
∀(zero : natural) →
natural
) →
Natural
= Natural/build

let example0 =
assert
: build
( λ(natural : Type) →
λ(succ : naturalnatural) →
λ(zero : natural) →
succ (succ (succ zero))
)
≡ 3

let example1 =
assert
: build
( λ(natural : Type) →
λ(succ : naturalnatural) →
λ(zero : natural) →
zero
)
≡ 0

in build