24 lines
541 B
Plaintext
24 lines
541 B
Plaintext
let Prelude = ./Prelude.dhall
|
|
|
|
let List/map = Prelude.List.map
|
|
|
|
let Preserves = ./Type.dhall
|
|
|
|
let Preserves/function = ./function.dhall
|
|
|
|
let record =
|
|
λ(label : Preserves) →
|
|
λ(fields : List Preserves) →
|
|
λ(Preserves : Type) →
|
|
λ(value : Preserves/function Preserves) →
|
|
value.record
|
|
(label Preserves value)
|
|
( List/map
|
|
Preserves@1
|
|
Preserves
|
|
(λ(value : Preserves@1) → value Preserves value@1)
|
|
fields
|
|
)
|
|
|
|
in record
|