coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Ltac: match and constr_list?

From: Scott Lawrence <srl AT umd.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Ltac: match and constr_list?
Date: Sat, 29 Dec 2018 12:48:51 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=bytbox AT gmail.com; spf=Pass smtp.mailfrom=bytbox AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f172.google.com
Ironport-phdr: 9a23:yhd51hBzA0ms+b21MAnDUyQJP3N1i/DPJgcQr6AfoPdwSPv7p8bcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoHLD03/nzXhMJugqxUvByuqBNwzYPPfIGYNuBzcr/Bcd4AR2dMWNtaWSxbAoO7aosCF/cPMvpfr4nhu1sFsB2wChOiBeP11DBIgGP50rMn2OkmCgHGxgggEskTsHTRsdr5LrkdXv2ozKTRyzjIcvBY2S/l5YTWbhwspeuAULFwfMbL1EUiFh/Jgk+NpYHnIT+ZzvkBv3SH4+Z6SO6ii3QrpxxsrjWr3MshhIvEi4QIwV7e7yp52pw6JdigRU57f9GkFJxQujmfN4RsQ8MiR3hkuD8myrEboJK7cjUGxZY5yxLFZPyHdI+I4h3nVOmPOzt3mHVleLenixaz90iv1PH8W9Gq3FpWqidJiNrBu3AX2xDO68WLVuFx8lqj1DqRzwzT7/tLIUEwlarVMZ4hxbswm4IIvkXDAi/5g0L2jaCNe0Ur/+in8eXnYrH8qpCAMI90jxnyMr4ylcynHeQ4Lg8OUnCH9uS7zb3v5FH2QLFXjvItiaTZq5DbJcEDpqGjGQNV04Aj6wy+Dzi8ytgYk2MHfxp5f0eMiJGsMFXTKtj5C+2+ihKiimRF3ffDa4bqBYnRZlzKj63se71woxpH0g4b0NVToZ9YF+dSc7rIRkbtuYmAXVcCOAuuzrO/UYQv5sYlQWuKR5ShHubXuF6M6PgoJrDVNoAQsTf5bfMi4qy31CNrqRomZaCsmKAvRjWgBP0/eheWZHPthpEKFmJY5lNjHtyvs0WLVHtoX1j3X6844WtlWoevDIOGX5z0xbLYg339EZpRaWRLTFuLFCWweg==

Hello all,

I'm attempting to write a tactic which is recursive on a variable-length
list of arguments. It seems that an argument matched (in Tactic Notation) by
constr_list cannot subsequently be inspected with `match`. Is there a way
around this, or do I need a plugin?

I have

Ltac tac_list' l := match l with
| _ => idtac "matched"
end.

and the notation

Tactic Notation "tac_list" constr_list(l) := tac_list' l.

Calling

tac_list' [1; 2].

of course works fine, but attempting to use the notation

tac_list 1 2.

yields

Must evaluate to a closed term
offending expression:
l
this is an object of type list

I'm guessing that "type list" does not refer to the coq "list" type?

Best,
Scott

[Coq-Club] Ltac: match and constr_list?, Scott Lawrence, 12/29/2018