The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/08/2015 12:21 AM, Jason Gross wrote:
> I do not have access to Coq at the moment, but does something like this
> work?
> Goal Type.
>    refine ((fun (x : nat) (y : _) => _) = (fun (x : nat) (y : _) => _)).

No - that actually loses its binders completely - which isn't what I 
would have expected either.  However, a variation of that is sufficient 
to create a case of what I was looking for:

Goal True.
  refine (let f := (fun (x : nat) (y : _ ) => _) in _); shelve_unifiable.

Thanks.
-- Jonathan

> On 1:11am, Wed, Jan 7, 2015 Jonathan Leivent 
> <jonikelee AT gmail.com>
>  wrote:
>
> > Is it possible in Coq for an evar instance to exist in a goal such that
> > it is "trapped" under binders?  Meaning that after all possible intros
> > are done, the evar instance still can't be found using Ltac's context[]
> > construct (as in [match .. with context[?V] => is_evar V ...], but
> > has_evar senses it)?  Any case of an evar instance "trapped" under
> > binders would seem to require that its type depends on bound variables.
> > I can construct such cases within the conclusion of a goal, but they
> > would become untrapped by doing sufficient intros, at which point
> > context[] can find them.  I can't seem to construct any cases in
> > hypotheses (trapped under vars bound in the hypothesis), however.  But,
> > that's certainly not proof that it isn't possible.
> >
> > If such trapped evar instances are possible, can anyone come up with an
> > example?
> >
> > -- Jonathan