[Agda] Re: A patch making Agda smaller and faster

[Nils Anders Danielsson]

On Wed, Mar 5, 2008 at 1:18 PM, Makoto Takeyama
<makoto.takeyama at aist.go.jp> wrote:
>
>  - the max resident memory size shown by Windows task manager becomes less
>   than half (839M -> 332M)

This is very nice! Now I can type check one of my formalisations
again, with "only" 1GB of RAM.

>  (If we get a chance to renovate Agda again, we should hash-cons
>  everything like (I believe) Coq does.)

I think Ulf plans to change from call-by-name to call-by-need. This
should improve sharing considerably.

-- 
/NAD