[Agda] termination by contradiction

[Ulf Norell]

On Fri, Jul 4, 2014 at 8:26 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:

> Objection, Ulf.
>
> NO_TERMINATION_CHECK is --no-termination-check, but for single definitions
> only.  The semantics should stay as is.
>
> 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.
>

Ok, fine. I guess we can have both. I do think that my version is more
important to have though. Disabling the termination checker and treating
definitions as terminating anyway is a hack that shouldn't be encouraged.
My version can be used safely (and soundly if paired with and inhabitation
check).

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140707/d6a916c6/attachment.html