[Agda] agda slow

[Andrea Vezzosi]

One hacky way would be to declare them coinductive, that would disable
eta but also pattern matching.

record Foo .. : Set where
   coinductive
   field
      bar : ...


Best,
Andrea


On Tue, Jun 2, 2015 at 6:03 PM, Thorsten Altenkirch
<Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> Hi,
>
> I know that this is a common experience. I was just starting to use some
> records to restructure some code we are working on and the memory goes
> through the roof. Is there a way to switch off eta expansion of records or
> would this disable type checking of records altogether.
>
> Cheers,
> Thorsten
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete it.
>
> Please do not use, copy or disclose the information contained in this
> message or in any attachment.  Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
>
> 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.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>