[Agda] Seg-fault

Serge D. Mechveliani mechvel at botik.ru
Sat Oct 13 21:32:15 CEST 2012

I have programmed the  merge sorting function  for a list over any 
with the result record including a proof for orderedness.

It is compiled for the RTS options, and run with  +RTS -M... -RTS.
For a certain large list over Nat, it finishes for  -M700m and 900m,  
but runs into  Segmentation fault  for 800m.

This is for  Agda- + MAlonzo + lib-0.6.


More information about the Agda mailing list