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: [Coq-Club] how to set a mutable field in an Ltac2 record
- Date: Fri, 21 Aug 2020 14:17:57 -0400
- 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-qt1-f176.google.com
- Ironport-phdr: 9a23:hoPG1RAa3Jyqho8wVxWDUyQJP3N1i/DPJgcQr6AfoPdwSPX6psbcNUDSrc9gkEXOFd2Cra4d1ayP6vqrADVYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmssAndq9cajYR/Jqos1hfCv2dFdflRyW50P1yYggzy5t23/J5t8iRQv+wu+stdWqjkfKo2UKJVAi0+P286+MPkux/DTRCS5nQHSWUZjgBIAwne4x7kWJr6rzb3ufB82CmeOs32UKw0VDG/5KplVBPklCEKPCM//WrKiMJ/kbhbrQqvqRJ/3YDafYKbOv1xcazBct0XXnZBU8RLWiBdGI6wc5UDAuwcNuhYtYn9oF4OoAOwCQmuA+PvzD5Ihnzo0q0+zesuDxrL3AMlH90UsXTUqM/5O7sVUeCwwqXD0DLOb/FR2Tf76YjIcQ4uofWSUr1uasfRxkwvGBnEjlWUs4DqIzSV1uEUvmWd8uFvWv6hhXQ9pAFtvjig2N0sio/Ri44Iyl3K9Sp0zZgpKdCkSEN2Y9CpHYdfui2GN4Z6X80sT31stSs7yrMLuoC2cDQWxZk62RLSaeCKfpWG7x/jWuicJypzinF9eL+nmRq+7Uytxvf/W8S0ylpGsytInsXWunwQ1RHe69CLRuV880u9xDqC0h3f5+VYLk0xmqfWKoItzqI1m5YOr0jDECr7mEvqg6CIeEUp//Kn5PnpYrXoo5KcOZF7hRzkPakrhsOyAOo1PwoIUmOG4+qzzqfj8lf8QLhSjv05jK3ZsJfCKMQevKG5AgtV3p866xajEjuqydoYkWQFIV9EYh6HgI/pO1bBIPD8E/izmUijkDBux/zeP73hBIvCLmTbnbv/Ybpw71RQxQkzwNxF+p5ZC60NLOjuVkLztdHUFho5PBa1w+bjBtV9zIQeWWeXD6+bN6PSt16I5uExLOmIeoAapi3wK/cg5/H0jH85nUURcrWu3ZsScHy4BOhpI12FYXrwhdcMCXsFvg0nTODzlFKCVSNTaG2pUqIn5jA7DZqmAp3ZSoCshryBxia7EYdMamBIEFDfWUvvIo6DQrIHbD+YaptqlSVBXry8Qacg0wuvvUn00ew0APDT/3hSt5Xl1dt44+DevR43/D1wSc+a1ivFG2NzmGILSjs70YhwpEV8zhGI1q0u0K8QLsBa+/4cClRyDpXb1eEvU4mvCDKERc+ATROdevvjATw1SYhvkdoHYkI4Asn7yx6agHTsDLgSmLiGQpcz9/CEhimjF4NG03/DkZIZoRwjS8pLO3ehg/cmpQfWDo/N1U6ekvTzLPhO7Gv27G6GiFG2kgRASgcpCPfKWHkeYg3dqtGrvk4=
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?
- [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+.