The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This is untested, but I think the following should work:

lazymatch goal with

  | [ |- ?lhs = ?e ?x ] => let lhs' := (eval pattern x in lhs) in change (lhs' = e x)

end

 

On Fri, Jul 25, 2014 at 5:08 PM, Jonathan <jonikelee AT gmail.com> wrote:

Suppose one has a goal of the form:

  <some _expression_ with free X> = ?42 X

where ?42 is an evar with the proper function type.  Is there a way to abstract out X from just the lhs of the equality (via beta expansion)?  Like a variant of pattern that could be focused on just the lhs of the equality, allowing ?42 X to unify easily with the resulting beta-expansion?

-- Jonathan