11 lines
235 B
Plaintext
11 lines
235 B
Plaintext
|
{-|
|
||
|
Dhall encoding of an arbitrary Preserves value
|
||
|
-}
|
||
|
let Preserves/function = ./function.dhall
|
||
|
|
||
|
let Preserves/Type
|
||
|
: Type
|
||
|
= ∀(Preserves : Type) → ∀(value : Preserves/function Preserves) → Preserves
|
||
|
|
||
|
in Preserves/Type
|