16 lines
336 B
Plaintext
16 lines
336 B
Plaintext
{-|
|
|
Create an embedded Preserves value.
|
|
-}
|
|
let Preserves = ./Type.dhall
|
|
|
|
let Preserves/function = ./function.dhall
|
|
|
|
let embedded
|
|
: Preserves → Preserves
|
|
= λ(value : Preserves) →
|
|
λ(Preserves : Type) →
|
|
λ(value : Preserves/function Preserves) →
|
|
value.embedded (value@1 Preserves value)
|
|
|
|
in embedded
|