Ssreflect Users Discussion List

[Georges Gonthier <>]

> I am a little confused about what is written in Sec 2.5 of the document:
> "it enhances the possibilities of using such wildcards."

> Axiom f_p: forall a1 a2, p a1 -> p a2 -> p (g a1 2).

> Goal p a ->True.
  move/f_p.

> Something clever is happening :-)

Namely, that unresolved wildcards are generalized, as in the ML let, rather 
than generating a type error outright.

> I am aware that the following script fails.

> Goal p a ->True.
> move => pa. generalize (f_p pa).

True, but
  have:= f_p pa.
will work, because have also performs this ML-let-style treatment of 
wildcards. Note that
  move: (f_p pa).
will not work, however, because move attempts to fill wildcards by matching a 
subterm in the goal.

Georges