Ssreflect Users Discussion List

[Jason Gross <>]

Thanks.

Georges has told me that another way to do this is case/(@id bool), which I think is what I'll stick with for now.

-Jason

On Wed, Jun 11, 2014 at 1:32 PM, Enrico Tassi <> wrote:

On Wed, Jun 11, 2014 at 12:01:02PM +0100, Jason Gross wrote:
> Hi,
>
> Is there a variant of case/boolP that does not error on the following?
>
> Goal forall b : bool, b = b.
>   case/boolP.

What goes wrong in your code is not the "dependent type" but the fact
that b is cleared (and cannot).  This works:

  move=> b; case/boolP: (b).

Note the extra () around b.

Ciao
--
Enrico Tassi