coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] simpl as a function

From: t x <txrev319 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] simpl as a function
Date: Sun, 18 Aug 2013 13:53:24 +0000

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!

[Coq-Club] simpl as a function, t x, 08/18/2013
- Re: [Coq-Club] simpl as a function, Jason Gross, 08/18/2013
  - Re: [Coq-Club] simpl as a function, t x, 08/18/2013
    - Re: [Coq-Club] simpl as a function, Adam Chlipala, 08/18/2013