The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 24 Oct 2013 17:27:33 -0200,
Marcus Ramos 
<marcus.ramos AT univasf.edu.br>
 a écrit :

> Hi Auger,
> 
> Thank you for the reply and the hint, now I understand it. Also for
> the suggestion of flipping the bit, but my main concern is indeed the
> proof, not the function itself.

The proof is also easier. There are only two cases to explore (one for
each value of the bit), rather than more than two hundred.

> 
> On the other hand, do you know where I can get an explanation of the
> semantics of "intros [[][][][][][][][]]"?

intros [[][][][][][][][]].
is equivalent to
intros x; case x as [[][][][][][][][]].

For nat, for instance you can do:
intros [|pred].
equivalent to:
intros n; case n as [|pred].

> Neither the Reference
> Manual nor Coq'Art helped me in that. Is there an alternative way of
> splitting all 256 goals?

Flip the bit, so that you will need only 2 goals instead of the 256
you get by using your conversion functions.

> 
> Best Regards,
> Marcus.