[Agda] COMPILED_DATA directive for Maybe

[Nils Anders Danielsson]

On 2009-11-23 22:24, Dan Doel wrote:
>   build : {i : Level}{A : Set i}
>         -> ({j : Level}{R : Set j} -> (A -> R -> R) -> R -> R)
>         -> List A
>   build k = k _::_ []

Do you have any interesting use cases for build in the absence of
parametricity?

--
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.