31 lines
724 B
Text
31 lines
724 B
Text
|
--| `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
|