Ssreflect Users Discussion List

[<>]

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

That would imply that as long as the application is saturated at the end,
I will not get such type error. This is a simple criterion I can keep in 
mind. 
 
> > 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.

Perhaps I prefer only to use "move/f_p", but not to set Implicit Arguments.
Thus I avoid having two semantics for the application.

Best,
Keiko