The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

As far as the kernel is concerned this is possible but the syntax is not 
done yet. See https://github.com/coq/coq/pull/7651

Gaëtan Gilbert

On 01/11/2018 12:21, Thorsten Altenkirch wrote:
> Is there a way to run possibly non-terminating programs in the coq type 
> checker. In Agda you can just switch off the termination checker.
>
> I think this is useful if you want to use something whose termination 
> you haven't yet proven but want to exploit reduction.
>
> Hence it is not enough to add the assumption that it terminates as an 
> axiom because this won't reduce.
>
> Thorsten
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.