coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Emilio Jesús Gallego Arias <e AT x80.org>
- To: Joachim Breitner <mail AT joachim-breitner.de>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Proof-local LTac
- Date: Mon, 07 May 2018 16:06:25 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
- Ironport-phdr: 9a23:TXve7RfL/NNZHPxjYv/Ho+zclGMj4u6mDksu8pMizoh2WeGdxcu7bB7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNF3jKJVrhyupR9xzIDbb46JO/RzZb/dfcoASGZdQspcTS5MD4WhZIUPFeoBOuNYopHyqVsLrBu+AQisBOT3xTFMmHD2xrci0/85Hg/HxgMgG9YOv2rbrNXyLKgfTfq1zKjSwjXYcvhb3iny5ZPHcx0ivf2AR7VwcdDeyUQ2EQ7Ok1aeqZT9Mj+I1ekAsHKX4/R+We+ukWIrtgN8riW1yssxhITFmJoZx1LG+Clj3Yo4Jd61RFRmbdOnDJdcrT+WOoRqTs4kXmpmojw1yqcctp6+ZCUKyIooxxrYa/GffImF4Q7vWPyWITdii3JpYLO/hxCs/ki80uDwS8q53VVQoiZbjNXBt2oB2wHR58SaUPdx40ms1SiX2wDW8O5EIEQ0laTBK54mx749joQcvF/MHyL1hEn6lqiWdl8r+uSw8eTofq3mpoOAN49zkgzxLqMumtWmDeskNggOQnOU9P+n1Lzj+E35WK9Fguc3kqnfqpDaJN4UqrS3Aw9Pgc4f7EOdCD6t0NUd1VMdIVNZfh+dx9zsMlDKCPL/BPy/glHpmi1mxuzAM6enDpibfVbZl7K0ULN8709b/yg+1kJE0L1dDrUML/XEc1XwvceQWhIRI1zsheH9B4MuhcslRWuTD/rBY+vpuliS67d3erjeVMouoD/4bsMdybvrhH49l0UaePj7zctPLneiEaY/ehnLUT/Xmt4EVFwykE8mVuW72k3SCXhUfXngB/thtAF+M5qvCML4fq7ogLGF23bpDs0OIGdcBQLVHA==
- Organization: X80 Heavy Industries
Joachim Breitner
<mail AT joachim-breitner.de>
writes:
> Lemma …
> Proof.
> Ltac foo := …
> …
> Qed.
>
> and was very surprised when later someone else working on the same
> project started using the `foo` tactic in a different proof further
> down.
Indeed, as of today any command with "side effects" gets replayed
outside the proof as if the script was:
Lemma …
Admitted.
Ltac foo := …
> Also, I noticed that an Ltac definition inside a Proof cannot mention
> local variables, so I cannot do
That's due to the above semantics.
IMHO, you should avoid performing actions with global effects inside
proofs, at least for the moment, as this is considered "fragile" and is
an area where semantics might change soon.
> Is there a way to define proof-local ltacs that capture local
> variables?
That I don't know.
E.
- [Coq-Club] Proof-local LTac, Joachim Breitner, 05/07/2018
- Re: [Coq-Club] Proof-local LTac, Emilio Jesús Gallego Arias, 05/07/2018
Archive powered by MHonArc 2.6.18.