The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Hello,

Le 15 juin 08 à 12:00, 
frederic.blanqui AT loria.fr
 a écrit :

> On Fri, 13 Jun 2008, 
> frederic.blanqui AT loria.fr
>  wrote:
>
> > Hello. As it is well known, many function definitions are rejected  
> > by Coq since they do not pass Coq termination checker which accepts  
> > only structurally terminating functions. Would it be possible to  
> > add a new command line option to coqc that would disable the  
> > termination checker?
>
> Instead of a command line option, it would be better to have a  
> command like "Unsafe Fixpoint" to disable the termination check  
> locally and keep a trace of this in the file itself.

Actually, one would still need to tell on which argument to recurse,  
as the reduction functions need this to decide when to unfold. So I  
think a { general x } annotation would be the right way to do it. I'm  
willing to make the change (I have a patch somewhere doing that  
already), but maybe there are some arguments against it?

--
Matthieu Sozeau
http://www.lri.fr/~sozeau