The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2015-03-30 1:16 GMT+02:00 Matthieu Sozeau 
<mattam AT mattam.org>:
> Hi Zoe,
>
>   the classic answer is to build an unfolded version (without Program and
> which
> calls the folded version at recursive calls) and show extensional
> equivalence of
> the two definitions, then you can easily control unfolding using rewriting,
> and
> avoid the clutter due to decoration of matches with equalities at matches.
> Otherwise you might find the [lazy] reduction strategy useful, but mainly
> for
> full normalization. [Function] might help too but I couldn't manage to make
> it work on this example.


Hi,

Indeed the example triggered a bug in Function that is under
investigation. The initial example should go through untouched with
simpl (actually I does when bypassing the exception raised by the
bug).

Best
Pierre