22 lines
500 B
Plaintext
22 lines
500 B
Plaintext
{-|
|
|
Create a Preserves sequence value from a `List` of values and a conversion function
|
|
|
|
See ./render.dhall for an example.
|
|
-}
|
|
let Prelude = ./Prelude.dhall
|
|
|
|
let List/map = Prelude.List.map
|
|
|
|
let Preserves = ./Type.dhall
|
|
|
|
let Preserves/sequence = ./sequence.dhall
|
|
|
|
let sequenceOf
|
|
: ∀(a : Type) → (a → Preserves) → List a → Preserves
|
|
= λ(a : Type) →
|
|
λ(f : a → Preserves) →
|
|
λ(xs : List a) →
|
|
Preserves/sequence (List/map a Preserves f xs)
|
|
|
|
in sequenceOf
|