POSTUlATE_TERMINATION --- Was: Re: [Agda] termination by contradiction

[Wolfram Kahl]

On Fri, Jul 04, 2014 at 08:12:44PM +0200, Ulf Norell wrote:
> The --no-termination-check flag will still treat functions as terminating.
> The motivation for the
> new behaviour (which I honestly thought was the intended behaviour all
> along) is to let you
> write possibly non-terminating programs without jeopardising decidability
> of type checking.

Perhaps a POSTULATE_TERMINATION pragma might be useful;
with the intention that this would be used for terminating functions
that the (current) termination checker does not recognise as such.
The type checker would trust this just like a postulate;
this of course means that if the function in question does in fact
not terminate, the type checker will loop.
Just like with postulates, *.agdai files should then also be generated.
Theoretically, the definition could be considered as given via
Induction.* with postulates for the relevant wellfoundedness properties.
(``safe'' mode should of course reject it.)


Wolfram