[Agda] type check cost

[Nils Anders Danielsson]

On 2015-10-04 15:57, mechvel at scico.botik.ru wrote:
> Currently I use  Agda 2.4.2.4  to develop my algebraic library called DoCon-A.
> And it cannot type-check on a machine of  16 Gb RAM.

During the last Agda meeting we implemented some optimisations that
might be useful for you. However, AFAIR they have not been released yet.
I suggest that you try the development version of Agda.

-- 
/NAD