The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Does the ltac [let H0' := (eval simpl in H0) in set (H0'' := H0')] do what you want?  Alternatively, if you are trying to construct a proof without ltac, [Definition foo := Eval simpl in <_expression_>.]

-Jason

On Aug 18, 2013 9:53 AM, "t x" <txrev319 AT gmail.com> wrote:

Is there a Coq function which does the same as simpl?

I.e. "simpl in H0" vs (set H0 := magic_function H0)

I'm playing around with pattern matching / trying to construct proofs by functions -- and I find myself constantly wanting to have a "simpl" function to simplify terms.

Thanks!