The Coq mailing list

[Adam James Chlipala <adamc AT EECS.Berkeley.EDU>]

The variable 'n' is rebound in the 'S n' branch of the pattern match.

----- Original Message -----
From: Jimmy Miller 
<captainthunder AT gmail.com>

> 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?