Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Apr 02, 2014 at 09:48:00PM +0000, Georges Gonthier wrote:
> Try case/(_ _)/Wrap. -Georges

Let me disassemble it.

  move=> top; case: (Wrap(top _)).

where Wrap(top _) has type (wrapped Q), hence matching on it gives you Q.

Wrap is there just to let you call the case tactic that has a very
specific behavior w.r.t. _ occurring in the scrutinee: open a new goal
for it.  It comes from the fact that one may want to case on a term h of
type A -> B /\ C, that requires a proof of A in order to obtain the
inductive.

On the contrary, move generalizes _ away.

  move=> top; move: (Wrap(top _))

is very much like writing

  move=> top; move: (fun p => Wrap(top p))

that leaves on the stack

  (P -> wrapped Q) -> R

and if you remove the Wrap, you have just the no-op you were obtaining
by writing move/(_ _), that disassembles to:

  move=> top; move: (top _).

Hope it helps...
-- 
Enrico Tassi