Ssreflect Users Discussion List

[Jason Gross <>]

Indeed, that helps.

I'm trying to have [case], but only when the term being cased unifies with [and _ _].  I was hoping for something like

do ![ case/(@id (ex _))

     | case/(@id (and _ _))

     | move => ? ]

to intro everything, destructing anything of type [ex _] or [and _ _] along the way.

-Jason

On Thu, Jun 26, 2014 at 4:49 PM, Enrico Tassi <> wrote:

On Thu, Jun 26, 2014 at 04:34:27PM +0100, Jason Gross wrote:
> Hi,
> The following code fails with "Error: Not an inductive product":
>
> Require Import ssreflect. (* v 1.4 *)
> Goal forall A B, A /\ B -> True.
>     move => A B.
>     case/(@id (and _ _)).

I hope that this decompilation helps you understand what goes wrong:

  Goal forall A B, A /\ B -> True.
  move => A B.

  have xx := @id (and _ _).
  move/xx.
  case.

Given that "xx : forall P P0 : Prop, P /\ P0 -> P /\ P0", the first
premise "A /\ B" can play the role of P, being of type Prop.

But the real question is: what are you trying to do?

Best,
--
Enrico Tassi