The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

[eq_rect] is the "rewrite function".  Unification is insufficiently powerful to auto-infer all the terms that you want inferred.  See also the notations "rew H in <term>", "rew <- H in <term>", "rew -> H in <term>" (also "rew H at <n> in <term>") which are apparently written in ml.

-Jason

On Wednesday, August 21, 2013, t x wrote:

I want the rewrite tactic as a rewrite function.

https://gist.github.com/anonymous/6299963

Line 32 correctly does the rewrite I want.

Line 14 fails the rewrite, likely beacuse in line 3, (fun X => _) ends up being (fun X => H) rather than (fun X => X + b = 10).

I believe the process I want is called "beta expansion". Is there a way to fix type_rewrite so that line 14 behaves like line 32?

Thanks!