[Agda] termination by contradiction

[Nicolas Pouillard]

Quoting Ulf Norell (2014-07-07 06:16:19)
> 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).

I'm standing with Andreas on the semantics for NO_TERMINATION_CHECK to be the
same as --no-termination-check local to some definitions.

Then as of having two pragmas it then raises the question whether there should
be a NON_TERMINATING pragma or something to be used together with
NO_TERMINATION_CHECK to tell Agda to not unfold. Then as mentioned abstract is
here for that.