coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rename bound variable

From: Laurent Thery <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] rename bound variable
Date: Mon, 10 Feb 2025 02:33:45 +0100
Authentication-results: mail3-relais-sop.national.inria.fr; dkim=none (message not signed) header.i=none; spf=None smtp.mailfrom=thery AT sophia.inria.fr; dmarc=fail (p=none dis=none) d=inria.fr

Goal exists n, n = 0.
refine (_ : exists nn, _).

seems to work

On 2/10/25 2:10 AM, Abhishek Anand wrote:

Is there a way to rename a bound variable?
For example, when proving the goal |exists n:nat, n=1|, can I ask Coq to rename n to nn?
I guess it can be done in Ltac2 by creating an alpha equal constr with the desired name and asserting it. I am wondering whether someone has already written something to achieve this.

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/ <http://www.cs.cornell.edu/~aa755/>

[Coq-Club] rename bound variable, Abhishek Anand, 02/10/2025
- Re: [Coq-Club] rename bound variable, Laurent Thery, 02/10/2025