[Agda] Compiler internals for projection functions

[Alan Jeffrey]

Ah, this is related to the recent performance gains. I'd say that's a 
pretty benefit for a minor bump in the road for the JS FFI. I'll try to 
come up with a form of words which describes when arguments may end up 
with dummy values.

A.

On 09/23/2011 03:34 AM, Ulf Norell wrote:
>
> On Fri, Sep 23, 2011 at 10:21 AM, Vincent Siles
> <vincent.siles at ens-lyon.org <mailto:vincent.siles at ens-lyon.org>> wrote:
>
>     Is this related to the performance issue  you were talking about a
>     few week ago
>     (related to using Sigma instead of build-in records) ?
>
>
> Yes. With this optimisation using Sigma (record or datatype version) to
> define the
> type of categories doesn't make the type checker explode defining the
> projection functions.
>
> / Ulf