coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Turning an evar into a goal?

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Turning an evar into a goal?
Date: Sun, 2 Apr 2017 22:24:29 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f181.google.com
Ironport-phdr: 9a23:8/z/zhMyzQpda6aHl4Ul6mtUPXoX/o7sNwtQ0KIMzox0Lf//rarrMEGX3/hxlliBBdydsKMYzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFHiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkaKTA5/mHZhM9+gq1Vrx2upQBwzYHPbYGJNvdzZL/Rcc8USGdDWMtaSixPApm7b4sKF+cPOeFYr4/nqFsSrRuxHw+sD/7pxDBWh3/2w7M10+I9EQrb2wEgHdUOsHLVrNX2KqgSVf66w7fTwDXMavNZwzb96IzSfh89pvGMWKt9fMzMwkcsDwPIlkucpZDhMj+P1ekAs3KX4/R9We+ukWIrtgJ8riW3yssyhYTFnIMYxk3e+Sh6zos5P921RUp9bNW5CpVfrTuaOJFzQs46Q2FnpiI6yroetJ6+ZicKyZAnywfGa/ybb4SE+xzjWPuSLDtlnn5ld7W/hxG98Uik1OLwTNW70FFPriZdk9nMsG4C1wDL58SZVvdw+l2t1DWP2gzJ9O1IPEE5mbDGJ5Mi37I8jp8Tvl7CHi/ylkX2lqiWdkA89+iq7OTnZLTmppyCOI9wlA7xLL8jmsO6AesiMwgOW3KX9vi71L3m5UH5WqlFjuUqkqnFt5DXPdgUpqmgAwNMzokj7wu/ACy93dQDnXgHKUpFdwidg4joPVHOOvH4Au2lj1Siijc4j8zBa7bmG9DGKmXJuLbnZ7d0rUBGmyQpytUKxZVSA60BKfS7fkLwqtHeEldtMQuywuXqDNhw/owbUGOLRKSeNfWB4hez+uszLrzUN8cuszHnJq196g==

On 04/02/2017 09:52 PM, Jason Gross wrote:

Huh. That works in my toy example, but once again causes [Defined] to run
~forever in my actual example. Closing the proof with
all:exfalso; clear; admit. Grab Existential Variables. all:exfalso;
clear; admit. Time Defined.
right before the [let unused := ...] line in my actual example gives under
.2 seconds, whereas I haven't seen it terminate yet doing it after that
line.

I tend not to run into very long Defineds, so I don't have any experience working around them.

-- Jonathan

[Coq-Club] Turning an evar into a goal?, Jason Gross, 04/01/2017
- Re: [Coq-Club] Turning an evar into a goal?, Jonathan Leivent, 04/01/2017
  - Re: [Coq-Club] Turning an evar into a goal?, Jason Gross, 04/03/2017
    - Re: [Coq-Club] Turning an evar into a goal?, Jonathan Leivent, 04/03/2017
      - Re: [Coq-Club] Turning an evar into a goal?, Jason Gross, 04/03/2017
        
        Re: [Coq-Club] Turning an evar into a goal?, Jonathan Leivent, 04/03/2017