[Agda] termination by contradiction

[Andrés Sicard-Ramírez]

On 4 July 2014 13:26, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> If you want to declare a definition as non-terminating, please add a new
> pragma, like
>
>   {-# NON_TERMINATING bla #-}
>
> which informs Agda to not unfold bla.
>

I guess that using an abstract block + NO_TERMINATION_CHECK should be
enough.

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140705/2f053c7b/attachment.html