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

Copy path to clipboard

build is the inverse of fold

Examples

  build
Text
( λ(list : Type) →
λ(cons : Text → listlist) →
λ(nil : list) →
cons "ABC" (cons "DEF" nil)
)
≡ [ "ABC", "DEF" ]
  build
Text
(λ(list : Type) → λ(cons : Text → listlist) → λ(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 → listlist) →
λ(nil : list) →
cons "ABC" (cons "DEF" nil)
)
≡ [ "ABC", "DEF" ]

let example1 =
assert
: build
Text
( λ(list : Type) →
λ(cons : Text → listlist) →
λ(nil : list) →
nil
)
≡ ([] : List Text)

in build