coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?)
Date: Mon, 4 Feb 2019 08:02:34 +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-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:Eq2BPBG2YUHv0pb8akfsy51GYnF86YWxBRYc798ds5kLTJ7zoMiwAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4n/m/Klsx+gqFVoByjqBx+34Hab46aOeFifqzGZ94WWXZNUtpTWiFHH4iyb5EPD+0EPetAq4fyuUEOogW7BQisGejhxCVHh3Ht3a091eQqDAbL0gg+ENIUrnvUqdX0OL0cX++vwqjI1jLDb/VN1Djn7ojIbwotru+RUrJta8be01QvGhrDg16NqoLlJyuY2+sRv2SB8uZsSeCih3Q6pwx/oDWj3NoghpXUio4NxV3J8T91zJsxKNC4UkJ3fMCoHIdKuy2HOYZ7QdsuQ292tys51rELvJu2cSwJxZs8yBPSbuGLfoaW7R3+UeuRLyl3iXF5dL+6mRq96kagx+L6W8KpylhFtDBFncPJtn0V1xzc9MyHSvxl80q91zmByhzf5vxdLU4pl6XWJYctwrkrmZUNq0jDGTL2mFntg6+Ra0Uk/PWn5/7/YrX8oZ+cK5F7hR3iMqQvncy/B/40Mg8TX2iH/eS807rj/U7jTLpWif02l7HVsJHcJcsFuq60GwBY3po55xqiEzur0s4UkWQJIV9HYh6LkpTlN0zWLPD9F/i/glCskDlxx/DBO73sGpHDIWbZkLj/eLZ861RQxgQpwtFR/JJUDbcBLenpVU/3qdzUFAE2PBGpw+r9Etp9y5sSWXiTDa+BLKPSrViI6/ozLOmLfY8ZoSryK/w45/H1lnI5gl8cfayx3ZQNcny4H/JmI1+YYXX2mNsBH30K7UICS7mgg1qbFDVXenyaXqQm5zh9BpjsRdPIQZnoi7ic1g+6GIdXbyZIEAbfP23vctCmVu0BbTPaDsZ+iTsCHeyDRpUs0ADomAbl0L1hBuPS52sVuY+l3cUjtL6brg076TEhV5fV6GqKVWwhxjpZFQ9z57h2pAlG8nnG1KF5h/JCEtkKvaFAVBp8OJLBieVnWYmrBlDxO+yRQVPjee2IRCkrR4trkdYIfgBwF8jkhw2Rh3P3UY9QrKSCAdkPyoyZ33X1IJoimV/77/F4ymIXGY5IP2DggbNj/Q/OAYKPi1+ei6uhaaUb2mjK6XuHym2N+kpfVVwpXA==

On 02/04/2019 01:42 AM, Pierre Courtieu wrote:
>
> It is sais in documentation as far as I can tell: « applied to each goal
> independently means that is equivalent to 1:repeat solve_eqs. 2:repeat
> solve_eqs...

I'm not sure exactly which bit of the documentation you are referring
to, but there is no surprise to me in the fact that
all: repeat solve_eqs is equivalent to
1:repeat solve_eqs. 2:repeat solve_eqs

the surprise is that
all: solve_eqs is not equivalent to
1: solve_eqs. 2: solve_eqs

> But indeed we need a repeat with the interleaved semantics.
>
Could you describe this "interleaved semantics"? Is it what you were
referring to in saying "all:tac. applies the tac to all goals. Period."
and what I understood as "all:tac is a tactic which does a bit of
tac on each goal, then a bit more of tac on each goal, and so forth"?

> Can you fill a big report about that please?
>
"bug report'? No. Fortunately it seems that someone who understands
what you're referring to has done so.

Cheers,

Jeremy

Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?), Pierre Courtieu, 02/03/2019
- Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?), Théo Zimmermann, 02/03/2019
- Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?), Jeremy Dawson, 02/04/2019