coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
Archive powered by MhonArc 2.6.16.