The Coq mailing list

[Chantal Keller <chantal.keller AT wanadoo.fr>]

Hello,

You may look at the Ssreflect plugin [1], that gives among other
facilities to work with Booleans.

In standard Coq, you can do :
rewrite !andb_true_iff in H; destruct H as (Ha, (..., Hc)...)

Chantal.

[1] http://www.msr-inria.inria.fr/Projects/math-components




Le 07/11/2012 17:12, Nuno Gaspar a écrit :
> 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!
>