coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] clone evars in destruct

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] clone evars in destruct
Date: Fri, 15 Jan 2021 16:53:09 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f176.google.com
Ironport-phdr: 9a23:UO6JqRWAwYiQS8H88pSKgGUIqZDV8LGtZVwlr6E/grcLSJyIuqrYbB2Gt8tkgFKBZ4jH8fUM07OQ7/mxHzRaqs/b7zhCKMUKC0Zaz51O3kQJO42sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx8u42Pqv9JLNfg5GmCSyYa9oLBWxsA7dqtQajZFtJ6oszhbFuGdEd/pZyW91O16enQv36sOs8JJ+6ShdtO8t+sxaXanmY6g0SKFTASg7PWwy+MDlrwTIQxGV5nsbXGUWkx5IDBbA4RrnQJr/sTb0u/Rk1iWCMsL4Ub47WTK576d2UxDokzsINyQ48G7MlMN9ir9QrQ+7qBx+x47UZ5yVNOZ7c6jAc94WWXZNU8BMXCFHH4iybZYAD/AZMOhFsYf9qVsAoxiwCwaiC+zgyCNHiHDt0K0m0eksCx3K0BAuEt8MtnnfsdX7NL0VUeCw1KTF0zHDaOlT2Tjj7ojIbggur+uNXbJsaMbc100vGBnYjlqNt4PlOy6e2+MRvGiD7upgSf6gi2o9pAFsvzeg2MMsh5LGhoIQ0F/E9CF5zJwpKt2/TU52eNipG4ZfuC+GLYV5WN8iQ312tyYgzL0LoYK3cSwExpop2hLSavOKfouU7x//W+ucPTd1iXFqdr+ihxi/8EytxvD8W8SqzFtHoSpIn9vIu30T1BHd5cmKR/9780y82jiPzxje5v9YLU0wj6bWKJ4szqQtmpcSrUjPBDL6lUf3gaOOaEkp9fKk5uX6brn8uJOROJN4hhv9P6gynMG0HP42PRIUX2eB/OSxzL3j8lP9QLVNlvA2l7PWsJHeJcgCv665HxJZ3p8t6xqiDTqr0c4UnXYALFJCdxKHi5bmN0vSL/D/CPezm1WskDF1yPDaJrDtHInBI3zZnLrifbtx8VNQxQsvwdxF+p5ZCLAMLOr2WkDrtdzYChE5Mxazw+biENhyypseWWOTAqCFNKPdq0KI6f8xLOmIf4IVtzP9JOIk5/7ql3M2hVgdfayx0ZsNdH+4BuhmI1meYXf0ntgBFn4KshMiQ+zulV2NSiVeZ22yXqI5/jE0EpiqDYbFRoC3gbyOxj23HpNMZjMONlfZGnDxMo6ARv0kaSSII8YnnCZXe6KmTtoK0ZCruQnm/IJmMq///iQFuZ/nnIx+/+zPnhU76DB5C+yS1miMSyd/mWZeFGx+57x2vUEokgTL6qN/mfENTYUPtcMMaR8zMNvn98I/E8r7A1uTcdKASVLgSdKjU2loE4ABhuQWakM4IO2MyxDO2y3wXe0Qnr2PQYUoq+fShievYcl6zHnC2e8qiFx0GpIeZ13jvbZ28k3oP6CMlkyYk6iwcqFFhXzC8W6CySyFu0QKCQM=

On 1/15/21 4:18 PM, Abhishek Anand wrote:
> Is there a way to ask destruct to clone some chosen evars for each case as
> I did below manually:

I use this:

Lemma xxx (b:bool): exists n, n = if b then 1 else 2.
eexists ?[x].
[x]: destruct b.

or this:

Lemma xxx (b:bool): exists n, n = if b then 1 else 2.
eexists; instantiate (1 := ltac:(destruct b)).

[Coq-Club] clone evars in destruct, Abhishek Anand, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Hugo Herbelin, 01/15/2021
  - Re: [Coq-Club] clone evars in destruct, jonikelee AT gmail.com, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Clément Pit-Claudel, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Siegfried, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Maximilian Wuttke, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Jeremy Dawson, 01/16/2021