coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] rewrite as a function instead of a tactic

From: t x <txrev319 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] rewrite as a function instead of a tactic
Date: Wed, 21 Aug 2013 20:43:58 +0000

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!

[Coq-Club] rewrite as a function instead of a tactic, t x, 08/21/2013
- Re: [Coq-Club] rewrite as a function instead of a tactic, Geoff Reedy, 08/22/2013
- Re: [Coq-Club] rewrite as a function instead of a tactic, Jason Gross, 08/22/2013