/Prelude-v16.0.0/List/build

Copy path to clipboard

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