The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello.

Is there a way to make specific functions not be reduced by simpl (even when they could be I mean..)?

For instance,

Example redtest:

  5 + 3 - 1 = 9.

Proof.

  simpl.

simpl will fully reduce the _expression_. What if I didn't want the minus function to reduce?

Sure, in this particular example I could do simpl plus, but I would like to be able to set this kind of "guard" for some functions, and also be able to unset them on demand.

I believe ssreflect does something similar, but I can't remember exactly how..

Help please :)

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.