coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] how to set a mutable field in an Ltac2 record
- Date: Fri, 21 Aug 2020 14:59:47 -0400
- Authentication-results: mail3-smtp-sop.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:AoImcRzKGOqXpPjXCy+O+j09IxM/srCxBDY+r6Qd2u8VIJqq85mqBkHD//Il1AaPAdyFrasd0aGP6v6ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTuwbalvIBmrswndudQajZZjJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lKxVrhK/qRJiwIDbYo+VOv1xcazBct0XXnZBU8RLWiBdGI6wc5UDAuwcNuhYtYn9oF4OoAOwCQmuA+PvzD5Ihnzo0q0+zesuDxrL3AMlH90UsXTUqM/5O7sVUeCwwqXD0DLOb/FR2Tf76YjIcQ4uofWSUr1uasfRxkwvGBnEjlWUs4DqIzSV1uEUvmWd8uFvWv6hhXQ9pAFtvjig2N0sio/Ri48X1l3K9Th0zYk7K9GlR0B1b9CpHYZfuiyGOIV7Rt4uTm52tSony7ALp5G1cigExZooxRPRZPyJfYeI7B//SeqcJypzinxieLK6nRmy8E6gx/XzVsm1zFZKrjdFncLWun8R0BzT786KQeZ+8Ee5wTuDyRzf5+VeLU03lafXMYAtzqAumpYJrEjOHCH7lF3ogKKXakko5+2l5/njb7r6o5KROI55hh3iPqkrh8CzH+o4Pw0AX2eH5+u82rju8lfkT7VEgP07l6fZv47HKssBo6O2Hw5Y34gh5hu5Ejyoys4XnWMdI1JAYB+Hj5bmO1XJIP3gCPewmVWskDNyy/DfPb3tH4zBLnbenLrjc7tx8UFcyA00zdBQ45JbFKsNL+70Wk/0rNDYDxk5PBKow+v/FtlxyocTVXiMD6KZKq/er0GE6vw1L+WRZoIYti7xK/0/6P7viX85l0Udfa6s3ZYPanC4GfJmI0SaYXXyhtcOD3kFsxExTOzvklKCUDpTa2yuUKI74zE3EJimApvbRoCxnLyB2z+2EYFRZmBfE1yDDXPod5ifVPoXcyKTIsphkiQeWrS7So8h0wuutA7gxLZ9IOrU4H5QiZW2399soubXiBt6oTdzFoGW13yHZ2ByhGIBATEsivNRu0t4nx2B1q55gPFcGNF76PZAUwN8PpnZhaQuCdf0WwHMetqEYFmjS9SiRzo2S4RikJc1f09hFoD63Vj41C2wDupNzuHZNNkP6qvZmkPJCYN9xnLBjvdzilAnRo5WNjTjiPcgrE7cAInGl0jfnKGvJ/xFgHz9sVybxG/Lh3l2FRZqWPycD38ab0rS69/+4xGaFu78OfEcKgJEjPW6BO5PY9ztg09BQa66atvbamO13Wy3AETRyw==
On Fri, 21 Aug 2020 14:17:57 -0400
"jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:
> The refman says: "Mutable fields of records can be modified using the
> set syntax." I see a set function for Arrays and Strings and a Set
> command for mutable global definitions, but nothing for mutable
> fields. No mentions of "set" in the refman's Ltac2 BNF either.
>
> Does anyone know what the mystery "set syntax" for mutable fields is?
>
Found it: "r.(field) := value". But now I am running into issue
https://github.com/coq/coq/issues/11086, so can't create a global
record with mutable fields anyway.
- [Coq-Club] how to set a mutable field in an Ltac2 record, jonikelee AT gmail.com, 08/21/2020
- Re: [Coq-Club] how to set a mutable field in an Ltac2 record, jonikelee AT gmail.com, 08/21/2020
Archive powered by MHonArc 2.6.19+.