coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Benoît Viguier <beviguier AT gmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>, vst-user AT lists.cs.princeton.edu
- Subject: [Coq-Club] Qed. does not terminate
- Date: Fri, 29 Jun 2018 11:49:08 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beviguier AT gmail.com; spf=Pass smtp.mailfrom=beviguier AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f49.google.com
- Ironport-phdr: 9a23:ggyi+BfwO4FoGvfQQEHvG1VKlGMj4u6mDksu8pMizoh2WeGdxcS7Yx7h7PlgxGXEQZ/co6odzbaO7ea4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYL5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM37mHZhNFzgqxVrh2uqABwzpXOb42JLvdzZL/RcN0YSGdHQ81fVzZBAoS5b4YXEucOI+BYr47zv1sStRSxCgisBOzyyj9JmHD2x7Ax3uM6Hg7YwgwgHt0OsGnVrNrrLqcfSu+1zKzSwjXCa/Nawyvy6I/Nch04p/yHQLx+cc3UyUY1FgPFiE2dqZLkPzOay+QNsnaU7/B6WeKpj24qrRx6rDu3xso0lIXFmoYYxkrH+Ch52oo5O8G0RU1hbdOrFJZcrzyWOoR2T884Xm1kpSc3xqcbtZO1ciUG0oorywPCZ/GBboOG+AjsVPyLLjd9nH9leKywhxK18UW4z+3zTMi00FJToiVbj9bAq2kB1xLc58WDUPd98UCh2TGA1wDX9O5IO1w7la3eK5I5w74wkIQcsVjbEyPohEn7iLWae0Yk9+Sy9ejrfrbrqoWTOoJwkg3+N74hms27AeQ2KAgOWG2b9Pyn27L94035QbpKjuA3kqbHqpDXPssbpqujDA9U1oYv8QqwDzCj0NgAh3kIMEpFeA6bj4juI1zBPPf4De6mj1uwlDdr2uvJM6b6ApTNK3jDiK3ucax8605a0gozzMpQ64haCrEbc7rPXRq7v9vBSxQ9LgacwuD9Cdw72JlUETaEBbbcO6fPu3eJ4PguKq+CftlR8CjmN704/PP0pXs4gkMGO6Kym4MNaXazE+hhJQOUbWe/rM0GFDIgsww5yvDdtlyNTD9efT7mVa8i5z4mCY+8JYjGT4GpxreG2XHoTdVtemlaBwXUQj/TfIKeVqJUMXPAEopaijUBEIOZZcok3BCquhX9zuM+fOXR8ywc85nk0YosvrGBpVQJ7TVxSv+l/SSVVWgtxzEHQjY32OZ0pkkvkg7eg5g9uORREJlo390MUgo+MsSBnelzCtS3Vw6YO9nVGRCpRdKpBTx3RdU0kYcD
Dear all, I'm faced with quite an anoying problem. I get my proofs in the
state "No more subgoals" totally fine. I did split my proofs into sub lemmas (I have about 14 of them). forward forward forward entailer! apply lemma_1; assumption forward rewrite ... 2: apply lemma_2 ; eauto forward ... I know that Opaque won't help as those are not visible by
the Type-checker. What can I do to solve this problem? -- Kind regards, Benoît Viguier Software Engineer - PhD Student | Cryptography & Formal Methods Radboud University | Mercator 1, room 03.17, Toernooiveld 212 6525 EC Nijmegen, the Netherlands | www.viguier.nl |
- [Coq-Club] Qed. does not terminate, Benoît Viguier, 06/29/2018
- Re: [Coq-Club] Qed. does not terminate, Fabian Kunze, 06/29/2018
Archive powered by MHonArc 2.6.18.