coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] "Sequence is associative." (?)
- Date: Thu, 24 Jan 2019 22:40:22 +0000
- Accept-language: en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:DLCufREVmXL4UJ966ztoaJ1GYnF86YWxBRYc798ds5kLTJ7yp8SwAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4n/m/Klsx+gqFVoByjqBx+34Hab46aOeFifqzGZ94WWXZNUtpTWiFHH4iyb5EPD+0EPetAq4fyuUEOogW7BQisGejhxCVHh3Ht3a091eQqDAbL0gg+ENIUrnvUqdX0OL0cX++vwqjI1jLDb/VN1Djn7ojIbwotru+RUrJta8be01QvGhrDg16Np4LlODaV2f4Ms2id9+dgVOSvi3Qmqw5ruDSvyN0sh4/UjYwW0lDJ7Sp0zJovKdGlVEJ2Y8SoHIZeuiybLYd6X94uT3xwtCs1zrAKo4O3cSwKxZg92hLTdeCLf5KV7h/tV+udOTl4i2xmdb6jghu/9Eytx+7nWcS71VtGsyRIncfRuX0I2Rzc9MuKRud480u/wjmP2Q/e5+dZKk4uj6XbMYQuwrsom5oTr0vDGij2lV3qgaCYa0so5vWk5/3gbLvpu5OQLoh0hRrgPag0ncy/HPg4PRMJX2iG/+Szyafv/VXjQLVNkv05jLXWsIzbJcQcoK61GQhV0ps/6xa7CDem19cYkWMbI1JCfRKLl4npO1fQL/DkFfqyjEignC12y/zaPLDtGIjBI3bCnbv7YLpx9lNQxBI2zd9F5pJUDr8BIOj0Wk/0rNHWCgE2MxaqzObiCNRxzI0QVniBA6+CN6PSt0SF6fgpI+mRfoMapivyK+U/6/H0kH81gUUdcrWx3ZsLdHC4GexrLFmeYXr1m9sODWMKvhclQ+Hxk12DUTtTZ26oUK4m5zE7DpimDYbZSYy3jryBxnTzIpoDLGtBExWHFWriX4SCQfYFLiyIaIc1mTsdELOlVoUJ1Be0tQa8xaAxfcTO/ShNl5/52d1kr8Haigo183QgLcmH3mScCU19gXgPQRc/2r05rEBgjF6eh/sry8dEHMBesqsaGjwxMoTRmrQjWoLCHznZd9LMc26IB9CvADU/VNU0moVcakBgXdiuk1bKwnjzWuNHp/mwHJUxt5nk8T3pPc8kkSTP0rRnglU7BMJSZzX/2/xPsjPLDouMqH230qancaNAg3zkyVzblC+rkRgdVwR9F6LYQXoYe03a68zj4V/PRKOvDrJhNRZdzcmFKe1Bbdi71Fg=
I'm puzzled by the reference in this document to, firstly,
for i = 0, ..., n
and secondly,
for i = 1, ..., n
Is one of these a typo, or what is the relevance of expr0?
And further down that page, it says
Variant expr0 ; [expri*|]
This variant of local tactic application is paired with a sequence.
In this variant, there must be as many expri as goals generated by the
application of expr0 to each of the individual goals independently. All
the above variants work in this form too. Formally, expr ; [ ... ] is
equivalent to [> expr ; [> ... ] .. ].
In this passage, what does "each of the individual goals" refer to?
And, what does the three dots refer to? Is a sort of meta-symbol,
whereas the two dots is something that is typed in literally?
And, by way of an illustrative example, what is the difference between
tac1 ; [ tac2 | tac3 ]
and
tac1 ; [> tac2 | tac3 ]
Thanks
Jeremy
On 01/24/2019 12:15 AM, Théo Zimmermann wrote:
> See
> https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.dispatch,
> for the documentation of [> foo .. ].
- [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Cao Qinxiang, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jean-Christophe Léchenet, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] "Sequence is associative." (?), Cao Qinxiang, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
Archive powered by MHonArc 2.6.18.