/Prelude-v21.1.0/List/build.dhall
Copy path to clipboardbuild
is the inverse of fold
Examples
build
Text
( λ(list : Type) →
λ(cons : Text → list → list) →
λ(nil : list) →
cons "ABC" (cons "DEF" nil)
)
≡ [ "ABC", "DEF" ]
build
Text
(λ(list : Type) → λ(cons : Text → list → list) → λ(nil : list) → nil)
≡ ([] : List Text)
Source
--| `build` is the inverse of `fold`
let build
: ∀(a : Type) →
(∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) →
List a
= List/build
let example0 =
assert
: build
Text
( λ(list : Type) →
λ(cons : Text → list → list) →
λ(nil : list) →
cons "ABC" (cons "DEF" nil)
)
≡ [ "ABC", "DEF" ]
let example1 =
assert
: build
Text
( λ(list : Type) →
λ(cons : Text → list → list) →
λ(nil : list) →
nil
)
≡ ([] : List Text)
in build