coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Can an Ltac2 tactic modify a top-level Ltac2 array?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Can an Ltac2 tactic modify a top-level Ltac2 array?
Date: Tue, 5 Jan 2021 16:36:25 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f173.google.com
Ironport-phdr: 9a23:NzQt9x0e9vEqNLA5smDT+DRfVm0co7zxezQtwd8ZseMWI/ad9pjvdHbS+e9qxAeQG9mCtLQe0LWd6vm7EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oMhm7owfcusYLjYd/JKs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9ZwgbpVrhyhuRJx3o3aboaaO/Vica3QZs8aRXNbU8pNTSFNHp2wYo0SBOQBJ+ZYqIz9qkMAoRu8AgmsAuLvyjxWiX/yw6I1zf8sEQ7D3AM6HtIOtG7Yo8nyNKcXX+y+0a7FzTfEb/NQ2Df965bHchQ/rv6SRr9wfs/RxlMuFwPBlFmftYvlPzaM2+kLrmOU4PZuW/i1hG47twF+vCKvxsE0h4fGm44YyFDJ+CRlzIspKtO1SUB1bNqqHpZTqy2XN5V6T8c+T29mtig21L8LtYC5cSULypkpyQPSZvOHfYaH4hzuUvuaLzRghH99Zr6zmxK//VKjx+D8TMW4zkhGojRfntXRtH0A2QTf5taGR/dh40us3CuD2gTP5exBLk05lLbXJ4Ikz7ItlZcesEHOETLqlErqgqKbc0Up+uam6+nibLXpuJ6RO5Fxhw7kMqkjntGzDOIlOQYURWeb4/6z1Lj78E35XrpKivo2n7HcsJ/AJMQbore1AxZW0oo+8hq/ASqq3dYWkHUdI1JFfxWHj4ftO17QOvz3EfC/g1G0nDdqwfDJIKHhD43TInTflLrtZ7Vw5k5GxAYt09xT+YhYBqwDLf/9QkPxscbXDh49Mwy62ebnD9B925scWWKIBK+ZMaDSvkGM5u0xPeaBf4AVuDPnJPgk4/7il2M2mVgYfaWxx5sYdGi4Huh6I0WeeXfjntABEX4TsgUiSOzqlUaNXCVIZ3eyWqI8/is0BJinDYfFXICtgaaO0D21Hp1MNSh6DQWHFm6tfIGZUb9YYyWLZ8RljzYsVL67SoZn2wv45yHgzL8yZOjT/CwbuJbu2fB64uTSkVc58jk+R5Cf1GeMTGxwk24gSDo/3aQ5qkt4nATQmZNkiuBVQIQAr8hCVR03YMaFnr5KTuvqUweERe+nDVOvQ9GoGzY0F4tjzNoHYkI7ENKn3EmagniaRoQNnrnOP6Qat6LR23+reZR4wnfCkbAi1hwoG5QUc2KhgaF7+k7YAIubyxzFxZbvTrwV2Wv2zEnG1XCH5RgKXwt5UKGDVncaNBPb

Does Ltac2 yet have the ability to modify something defined at
top-level from within a tactic? I can't seem to even define a
top-level Ltac2 definition with a mutable type. For instance (in
8.12.1), I get an error trying to do the following:

From Ltac2 Require Import Ltac2.
Ltac2 foo := Array.make 10 0.

With the cursor over "foo", the error is: "Error: Tactic definition
must be a syntactical value". Is this Ltac2's cryptic way of saying
that mutable arrays cannot be the values of top-level definitions?

[Coq-Club] Can an Ltac2 tactic modify a top-level Ltac2 array?, jonikelee AT gmail.com, 01/05/2021
- Re: [Coq-Club] Can an Ltac2 tactic modify a top-level Ltac2 array?, Pierre-Marie Pédrot, 01/05/2021
  - Re: [Coq-Club] Can an Ltac2 tactic modify a top-level Ltac2 array?, jonikelee AT gmail.com, 01/06/2021
    - Re: [Coq-Club] Can an Ltac2 tactic modify a top-level Ltac2 array?, Pierre-Marie Pédrot, 01/06/2021