The Coq mailing list

[Anton Trunov <anton.a.trunov AT gmail.com>]

Hi Thorsten,

There is a plugin written by Simon Boulier called TypingFlags:
https://github.com/SimonBoulier/TypingFlags

Best,
Anton

> On 1 Nov 2018, at 12:21, Thorsten Altenkirch 
> <Thorsten.Altenkirch AT nottingham.ac.uk>
>  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. 
> <image001.gif>
> 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.
> 
> 
> 
> 
>