Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, Jun 26, 2014 at 05:01:09PM +0100, Jason Gross wrote:
> 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 wayo.

Hum, I'm afraid the language is not designed for that.

Still you can enforce a typing constraint with something like

  move=> x; case: (x : _ /\ _) => pA pB {x}.

And such typing constraint is enforced using unification, and not
syntactic match as (I guess) Ltac match-goal-with would do.

Ciao
-- 
Enrico Tassi