The Coq mailing list

[Mathie <mathie AT gmail.com>]

I have defined the following function:

Require Import NArith.
Require Import Recdef.

Open Scope positive_scope.

Function factN (n : positive) {wf Plt n} : positive :=
match n with
| xH => xH
| xO x => n * factN ( Ppred n)
| xI x => n * factN ( Ppred n)
end.

(Proofs have been omitted.)

I'm having a bit of trouble trying to evaluate
factN 4:

Eval compute in (factN 4) 

results in a huge _expression_ rather than
a simple number.  

I know I'm missing something but I'm
not sure where to go from here.  Any
help will be greatly appreciated.