Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] "Sequence is associative." (?)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "Sequence is associative." (?)


Chronological Thread 
  • 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 .. ].



Archive powered by MHonArc 2.6.18.

Top of Page