<div dir="ltr">Using abstract doesn't work for a couple of reasons. One is that abstract is a module-wide construct, so things declared abstract will still unfold in the defining module. But, more importantly, as I explained above, I want a no termination check that is safe (that could at some point be allowed with --safe). Using the incredibly unsafe NO_TERMINATION_CHECK together with an abstract block doesn't fit that.<div>
<br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Jul 7, 2014 at 11:40 AM, Nicolas Pouillard <span dir="ltr"><<a href="mailto:np@nicolaspouillard.fr" target="_blank">np@nicolaspouillard.fr</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Quoting Ulf Norell (2014-07-07 06:16:19)<br>
<div><div class="h5">> On Fri, Jul 4, 2014 at 8:26 PM, Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>><br>
> wrote:<br>
><br>
> > Objection, Ulf.<br>
> ><br>
> > NO_TERMINATION_CHECK is --no-termination-check, but for single definitions<br>
> > only. The semantics should stay as is.<br>
> ><br>
> > If you want to declare a definition as non-terminating, please add a new<br>
> > pragma, like<br>
> ><br>
> > {-# NON_TERMINATING bla #-}<br>
> ><br>
> > which informs Agda to not unfold bla.<br>
> ><br>
><br>
> Ok, fine. I guess we can have both. I do think that my version is more<br>
> important to have though. Disabling the termination checker and treating<br>
> definitions as terminating anyway is a hack that shouldn't be encouraged.<br>
> My version can be used safely (and soundly if paired with and inhabitation<br>
> check).<br>
<br>
</div></div>I'm standing with Andreas on the semantics for NO_TERMINATION_CHECK to be the<br>
same as --no-termination-check local to some definitions.<br>
<br>
Then as of having two pragmas it then raises the question whether there should<br>
be a NON_TERMINATING pragma or something to be used together with<br>
NO_TERMINATION_CHECK to tell Agda to not unfold. Then as mentioned abstract is<br>
here for that.<br>
</blockquote></div><br></div>