The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Hello Everyone

While refactoring a development I came across the following (at least for me) 
surprising behavior:

Definition f (n:nat) := fix f m := match m with 0 => n | S m => f m end.
Fixpoint g (n m :nat) := match m with 0 => n | S m' => g n m' end.

Definition f3 := f 3.
Definition g3 := g 3.

Eval simpl in f3 3. (* = 3 *)
Eval simpl in g3 3. (* = g3 3 *)

I'm a little surprised that simpl unfolds f3 to expose and reduce the 
fix/match but not g3 and I would be interested in knowing why this is the 
case. 

Thanks in advance for any replies.

-- 
Regards
Christian