[Agda] AIM 10 notes

[Ulf Norell]

On Mon, Sep 21, 2009 at 10:41 AM, Conor McBride
<conor at strictlypositive.org>wrote:

>
> Meanwhile, on the postulates/implicit-rules question, might there
> be a third possibility? Should \uparrow compute through the
> structure of types? As it is, you may find traditional miseries
> arising, when (^ Nat) -> (^ Nat) turns out to be different from
> ^(Nat -> Nat). But perhaps you've got that covered..?
>

Indeed the lifting should distribute over function types.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090921/499cafea/attachment.html