[Agda] Circular proof causes stack overflow

[Nils Anders Danielsson]

On 2013-09-04 16:25, Dan Piponi wrote:
> This short piece of code causes a stack overflow in 2.3.2.1 (sometimes
> after a long wait):

The release notes for Agda 2.3.4 (which is under development) currently
contains the following text:

   Definitions which fail the termination checker are not unfolded any
   longer to avoid loops or stack overflows in Agda.  However, the
   termination checker for a mutual block is only invoked after
   type-checking, so there can still be loops if you define a
   non-terminating function.  But termination checking now happens
   before the other supplementary checks: positivity, polarity,
   injectivity and projection-likeness.
   Note that with the pragma {-# NO_TERMINATION_CHECK #-} you can make
   Agda treat any function as terminating.

-- 
/NAD