coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Factorial function

From: "Jimmy Miller" <captainthunder AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Factorial function
Date: Mon, 3 Sep 2007 10:39:32 -0500
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition; b=dhmYMEKWDOwjW36kO+5TQ1AptKuDi+MxvcCZk7n+nY8yQYFxwBmhRWgNHqT+JT1ls6cndRQ/XPu4NEgyT9/NCnQt/NJ1miAdOeL6ms46KvGmmt/D0ARAk6SauouXqGbMbiUf76Hpb984teEhN2ip9K7WvXDAn14oy4ol73xCWPA=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

In Coq.Arith.Factorial, the fact function is defined as follows:

Fixpoint fact (n:nat) : nat :=
  match n with
  | O => 1
  | S n => S n * fact n
  end.

But I'm having trouble understanding how this function works.  Usually
in a recursive factorial, fact is given n-1 each time it recurses, but
here I only see n getting passed to it.  Wouldn't this cause infinite
recursion, because fact gets the same argument every time, and thus n
will never reach 0?

If anyone can help me with this, I'd appreciate it.

--
<a href="http://www.spreadfirefox.com/?q=affiliates&id=153516&t=1";><textarea
rows="3" cols="40">Get Firefox!</a>

[Coq-Club] Factorial function, Jimmy Miller
- Re: [Coq-Club] Factorial function, Vincent Aravantinos
- Re: [Coq-Club] Factorial function, Adam James Chlipala