The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

There is the pattern tactic, but I do not know if there is a way to make it produce "(fun X => E) X = ?42 X" rather than "(fun X => E = ?42 X) X"

2014-07-25 18:08 GMT+02:00 Jonathan <jonikelee AT gmail.com>:

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

--
.../Sedrikov\...