coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] allowing non-structurally terminating functions ?

From: frederic.blanqui AT loria.fr
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] allowing non-structurally terminating functions ?
Date: Fri, 13 Jun 2008 11:32:12 +0200 (CEST)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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?

[Coq-Club] allowing non-structurally terminating functions ?, frederic . blanqui
- Re: [Coq-Club] allowing non-structurally terminating functions ?, Johannes Waldmann
- Re: [Coq-Club] allowing non-structurally terminating functions ?, Julien Forest
  - Re: [Coq-Club] allowing non-structurally terminating functions ?, frederic . blanqui
- [Coq-Club] Re: allowing non-structurally terminating functions ?, frederic . blanqui
  - Re: [Coq-Club] Re: allowing non-structurally terminating functions ?, Matthieu Sozeau
    - Re: [Coq-Club] Re: allowing non-structurally terminating functions ?, Arnaud Spiwack
      - Re: [Coq-Club] Re: allowing non-structurally terminating functions ?, Matthieu Sozeau
        
        Re: [Coq-Club] Re: allowing non-structurally terminating functions ?, courtieu
        
        Re: [Coq-Club] Re: allowing non-structurally terminating functions ?, Samuel Bronson
      - Re: [Coq-Club] Re: allowing non-structurally terminating functions ?, Julien Forest