Skip to Content.
Sympa Menu

coq-club - [Coq-Club] bool stuff

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] bool stuff


Chronological Thread 
  • From: Nuno Gaspar <nmpgaspar AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] bool stuff
  • Date: Wed, 7 Nov 2012 17:12:34 +0100

Hello.

Let's say that you have an hypothesis of this shape

H: A /\ B /\ ... /\ C

you could do 

destruct H as (Ha, (..., Hc)...).

Now, lets consider this hypothesis instead

H: A && B && ... && C = true

So, is there a tactic (or a general approach ...) that could allow me to easily obtain something like

Ha: A = true
...
Hc: C = true

?

Cheers!

--
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.



Archive powered by MHonArc 2.6.18.

Top of Page