38 lines
979 B
Plaintext
38 lines
979 B
Plaintext
{-|
|
|
Create a Preserves dictionary value from a Dhall `Map` of `Preserves` values
|
|
-}
|
|
let Prelude = ./Prelude.dhall
|
|
|
|
let List/map = Prelude.List.map
|
|
|
|
let Map/Entry = Prelude.Map.Entry
|
|
|
|
let Preserves = ./Type.dhall
|
|
|
|
let Preserves/function = ./function.dhall
|
|
|
|
let Preserves/Entry = Map/Entry Preserves Preserves
|
|
|
|
let Preserves/Map = List Preserves/Entry
|
|
|
|
let map
|
|
: Preserves/Map → Preserves
|
|
= λ(x : Preserves/Map) →
|
|
λ(Preserves : Type) →
|
|
let Preserves/Entry = Map/Entry Preserves Preserves
|
|
|
|
in λ(value : Preserves/function Preserves) →
|
|
value.dictionary
|
|
( List/map
|
|
Preserves/Entry@1
|
|
Preserves/Entry
|
|
( λ(e : Preserves/Entry@1) →
|
|
{ mapKey = e.mapKey Preserves value
|
|
, mapValue = e.mapValue Preserves value
|
|
}
|
|
)
|
|
x
|
|
)
|
|
|
|
in map
|