The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Gert Smolka wrote:
> Coq reduces terms like
>
> (fix f (y : bool) := y) t
>
> only if the argument term t starts with a constructor. The reference 
> manual hints that this constraint is needed
> to preserve strong normalization.
>
> I tried to construct an example that would justify the constraint
> but failed.  It seems to me that Coq restricts recursive applications
> such that they are always guarded by matches, and that this makes
> the constraint on fix reduction unnecessary.
>
> Is there an example that justifies the constraint on fix reduction?

Doesn't any recursive definition provide an example, since Coq's 
reduction is allowed inside [match] cases?