coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] bool stuff, Nuno Gaspar, 11/07/2012
- Re: [Coq-Club] bool stuff, Chantal Keller, 11/07/2012
- Re: [Coq-Club] bool stuff, gallais, 11/07/2012
- Re: [Coq-Club] bool stuff, Nuno Gaspar, 11/07/2012
Archive powered by MHonArc 2.6.18.