The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

Actually, Adam's book has some explanations and examples for the
various kinds of reduction in Coq:
http://adam.chlipala.net/cpdt/html/Equality.html

On Wed, Oct 23, 2013 at 10:38 PM, Catalin Hritcu
<catalin.hritcu AT gmail.com>
 wrote:
> The compute tactic is a lot more aggressive at reducing things than
> simpl. I'm not aware of any tutorial, but the Coq user manual has
> quite a bit about this:
>
> simpl only does beta, iota and expands transparent constants
> http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic135.
>
> compute does "cbv beta delta iota zeta"
> http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic129
>
> On Wed, Oct 23, 2013 at 8:55 PM, Marcus Ramos 
> <mvmramos AT gmail.com>
>  wrote:
>> Hi,
>>
>> Can anyone give me a link to a tutorial on the differences between "simpl"
>> and "compute"? I couldn´t find that myself.
>>
>> Thanks,
>> Marcus.