28 lines
620 B
Plaintext
28 lines
620 B
Plaintext
|
{-|
|
||
|
Create a Preserves sequence value from a `List` of `Preserve` values
|
||
|
|
||
|
See ./sequenceOf.dhall for an example.
|
||
|
-}
|
||
|
let Prelude = ./Prelude.dhall
|
||
|
|
||
|
let List/map = Prelude.List.map
|
||
|
|
||
|
let Preserves = ./Type.dhall
|
||
|
|
||
|
let Preserves/function = ./function.dhall
|
||
|
|
||
|
let sequence
|
||
|
: List Preserves → Preserves
|
||
|
= λ(x : List Preserves) →
|
||
|
λ(Preserves : Type) →
|
||
|
λ(value : Preserves/function Preserves) →
|
||
|
value.sequence
|
||
|
( List/map
|
||
|
Preserves@1
|
||
|
Preserves
|
||
|
(λ(value : Preserves@1) → value Preserves value@1)
|
||
|
x
|
||
|
)
|
||
|
|
||
|
in sequence
|