coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to write variadic tactics

From: Christopher Ernest Sally <christopherernestsally AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] How to write variadic tactics
Date: Tue, 18 Aug 2020 19:34:33 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=christopherernestsally AT gmail.com; spf=Pass smtp.mailfrom=christopherernestsally AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f49.google.com
Ironport-phdr: 9a23:K1lhsRepoCM5e2LBY8T4dpAtlGMj4u6mDksu8pMizoh2WeGdxcSzYh7h7PlgxGXEQZ/co6odzbaP7ea5ATNLusvJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRS7oR/MusUKg4ZuJag8xxvUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+uqBxxzYDXbo+IKvRxYrjQcskGSWdbRMtdSzBND4G6YoASD+QBJ+FYr4zlqlYQrRu+HwisBPjzyj9Pnn/23bM10/48Gg/JxgwgGcwBsG/IrN7oKakdS+S1zK3IzD7eaP5ZxTf96JLJchA6vfGMWqpwccrPxkk1CQzFlFOQppL+PzOJzeQCqWyb7+5gVO+0hG4nrht+ojmrxss2lobJgYcVx0nC+C5kz4k7Oce2R1RnYd64DpRQrSeaOpNoTs88QmxkpTo3x7wbtJOmeCUHxpUqyhHbZvGFfYaF4QzuWeSRLzp6hn9oeLCyiwux/EW+1+HwSNe53VJIoydLlNTHq3MD1wTL58SZVvdw+l2t1DWP2gzJ9+1JIEE5mbDUJpMlxLM7i4Advl7ZHiDsnUX7lK+WeVsg+uiv8+nnZ6/ppp6YN4NtiwH+NbkiltWxAek3NgUCRWeb+eO71L3s+U32Xq9GgeExkqncqJzaJMIbqbClAwJNzIov9xKyAy2l3dkYh3ULMVNIdROdg4XmP1zCOPX4Au2+g1Sonjdr3ffGPrj5D5rRLnjDirbhfa1h605b0Aozzc5Q54hKBbEbJvL8RFTxtMDDDhAjNwy0x+bmBc5y1oMbQ22PA6uZPLnOvl+P4+IjO/OMa5MNuDbhN/gl4ObjgmM+mV8EZKWmwZ8XaG2jEfl9OEWYYX/sgs8bHmsQvwo+SvbqiFyYXjJJaXayRfF02jZuA4W/SIzHW4rl1LeGxWKwGoBcTmFAEFGFV3nyIdaqQfAJPQmSOM56jjscVbW7A6I70xy1qEfBwr5jP6KA8S0CtIn/08B16vfejxc/7iBvBsCZwkmCSmh1miUDQDpgj/M3mlB01lrWifswuPdfD9EGv6oYADd/DobVyqlBM/63XwvAetmTT1P/G4epBDgwSpQ6xNpcOh8gSeXntQjK2m+RO5FQl7GPA8ZpoKfV3ny0JsEkjniahe8uiF4pRsYJPmqj1PYmq1rjQrXRmkDcrJ6EMLwG1XeUpmiGxGuK+kpfVVwoXA==

Hello Club

I'm looking to write variadic tactics ala clear, intros, destruct but inside coq, rather than ML.

I wanted to ask what was the best known methodology for this currently.

Thanks

Chris

[Coq-Club] How to write variadic tactics, Christopher Ernest Sally, 08/19/2020
- Re: [Coq-Club] How to write variadic tactics, Jason Gross, 08/19/2020
  - Re: [Coq-Club] How to write variadic tactics, jonikelee AT gmail.com, 08/19/2020
    - Re: [Coq-Club] How to write variadic tactics, jonikelee AT gmail.com, 08/19/2020