coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Termination

From: Gert Smolka <smolka AT ps.uni-saarland.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Termination
Date: Fri, 15 Jun 2012 08:29:06 +0200

One of our students discovered that Coq 8.3 accepts

Fixpoint foo (x : nat) : nat := (fun _ => O) (foo x).

although foo diverges under cbv.

Is this considered a bug or a feature?
(foo terminates under call by name)

Gert

[Coq-Club] Termination, Gert Smolka, 06/15/2012
- Re: [Coq-Club] Termination, Robbert Krebbers, 06/15/2012
- Re: [Coq-Club] Termination, Pierre Boutillier, 06/15/2012
  - Re: [Coq-Club] Termination, Tobias Tebbi, 06/19/2012