[Agda] Compiler internals for projection functions

[Ulf Norell]

On Fri, Sep 23, 2011 at 10:21 AM, Vincent Siles
<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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110923/790afadc/attachment.html