coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Tactic to collect hypothesis of given type in a list

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Tactic to collect hypothesis of given type in a list
Date: Thu, 15 Sep 2016 07:10:24 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga14.intel.com
Ironport-phdr: 9a23:H4fxpxywacE4xYHXCy+O+j09IxM/srCxBDY+r6Qd0eoRIJqq85mqBkHD//Il1AaPBtSCra0YwLOP7eigATVGusnR9ihaMdRlbFwst4Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbre9JomHxc+wzqW5/4DZSwROnju0J71oZl3ipgLI88ISnIFKK6AryxKPrGEeKMpMwmY9b2mUkhng/MCouNZG8i9Qsv8lvYYUVKTxf601SfpDCzkpL3oy/OXqswXOSU2E4X5KATZeqQZBHwWQtEKyZZz2qCav7uc=

Dear Jonathan, Beta,

Many thanks for the hints, especially the trick to do an ltac which changes
the goal and returns a value.

@Beta: I am experimenting with proof styles for something I want to integrate
into the standard library, so I fear I have to stick to what is available in
plain Coq.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Tactic to collect hypothesis of given type in a list, Soegtrop, Michael, 09/14/2016
- Re: [Coq-Club] Tactic to collect hypothesis of given type in a list, Jonathan Leivent, 09/14/2016
  - Re: [Coq-Club] Tactic to collect hypothesis of given type in a list, Beta Ziliani, 09/14/2016
    - RE: [Coq-Club] Tactic to collect hypothesis of given type in a list, Soegtrop, Michael, 09/15/2016
  - RE: [Coq-Club] Tactic to collect hypothesis of given type in a list, Soegtrop, Michael, 09/15/2016