coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Using patterns as arguments to Ltac tactics
- Date: Wed, 19 Jul 2023 18:00:55 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-pj1-f51.google.com
- Ironport-data: A9a23:I/MbeqxFnUI67ktGf996t+f4wirEfRIJ4+MujC+fZmUNrF6WrkVVy jRNX2yOaauMYmSgKNskbtzi8xkOsZPWyNc3HAZu+VhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefSAOCU5NfsYkhZXRVjRDoqlSVtkus4hp8AqdWiCmthg /uryyHkEAHjg2cc3l48sfrZ80sw5aWq4lv0g3RnDRx1lA+G/5UqJMlHTU2BByOQapVZGOe8W 9HCwNmRlo8O10pF5nuNy94XQ2VSKlLgFVDmZkl+B8BOtiN/Shkaic7XAhazhXB/0F1ll/gpo DlEWAfZpQ0BZsUgk8xFO/VU/r0X0QSrN9YrLFDm2fF/wXEqfFPwwahLJltuG7ZB99RJPmFx5 fMKFQ40O0Xra+KemNpXS8Fpj8UnadHpZcYR5ygmwjbeAvIrB5vERs0m5/cChGZ21p0IR6+AI ZdAAdZsREyojxlnIlYaEogz2uyvm2PjcjBFgF2QrKszpWPUyWSd1ZCzaYWKJYbUG625mG61m z3Iz3nkKSomNZ+azyCu2Gyymcv2yHaTtIU6TeXkrJaGmma7zWsKTRYSSFGTuui8kkf4WtRFK kVS9DBGkEQp3EmiT924Rx/h5XDZ51gTXN1fF+B84waIokbJ3+qHLnQGExtrcoQAj5Y7dwIV1 mCZkMHUOwU65dV5Vkmh3ruTqDqzPw0cImkDeTIIQGM5Dz/L8NBbYvXnHoYLLUKlsjHmMWqvn G3S/UDSk51W3JFbjfzqlbzSq2v0/sChc+Ij2unAsouYAu5RYYekY8mw6wGe46sZaomeSVaFs T4PnM32AAEy4XOlxXTlrAYlRunBCxO53Nv03wQH834JqW3FxpJbVdoMiAyS3W8wWir+RRfnY VXIpSRa74JJMX2hYMdfOtzhWptykPC7TYu6DJg4i+aihLAhJWdrGwk+NSatM5zFzSDAbIlla crFLZjyZZrkIf07nWrsLwvi7VPb7nlmmTm7qWHTwBOg3r6TDEN5up9UWGZimtsRtfveyC2Mq 4g3H5LTl313DralCgGJqtF7ELz/BSNnbXwAg5cKLrLrz8sPMD1JNsI9Npt7INc6xPkMzrmYl px/M2cBoGfCabT8AV3iQhhehHnHB/6TdFpqZnR+DkXiwHU5f4ek4YEWcpZ9L/Ft9/VuwbQwB 7MJctmJSKYHADnW2SUvXb+kpqxbdTOvmV2vOQiha2MBZJJOfVHC1eLlWQrNzxMwKBSLm/Ewm YD96TODc6E/H1xjKO30dMOQy0iAuClBueBqAGrNDNphWGTt14lILSbOoOc9CJwOI0+bxx+x9 QWfMTEHr8bj/q4399jog/ifjoGLSuFRIGtTL1P5352XaxbI3zOE6pBSdcq1ZhbhbXPQ1IT+Q PRK3tf+HeYinl0Xg7FjEr1u870y1+Hvq5Be0A5gOnfBNHavNZ9NPViE2ttppIRW57oEpzazZ F2DyuNaNZqNJsnhNlwbfyghT+ab0MAriivg1us0LGr69R1I0uK+C2sKBCa1iQtZMLdRG6Emy 714uMcptiqOuiBzOdOC1i1p52CAK0IbaJoet7YYPt7PqhEqwVR8c5DjGnfIwJWQWe5tbGguA BGp3ZTnuZoN53DsUXQJEVr14dF8nrUL4RBD808DLQ+Gm/3Dnf4G4ydS+jUWECVQwgl27OZoH m1NKUdOBL6v+g1wj5NpRFGcGABmBTyY9HfuylAPqnbrckmwWkHJL0w/Ieyo/n1F1055YR5g4 +i+5Ev+dDTlbuXd/3EXYlF0je7nQfha1BzwqOr+E+urR5AFMCfY2Imwbm82mj7bKMIWhmicg MJ1/ex1OJbJBQRJr4IVU4ClhKktEjaaL2l/QNZkzqMDPUfYXBqQgTGuCUSASvlhFszw032TK pJRf5pUdhGEyiyxgCgRBvcML59KjfcZ3oc+VY2xF1EWkYm0j2RPgMrL+znclV0bZYxksfwAJ 7P7cxOAFW2thkVopVLdkfkcOkSETIkFQCbewNGK9P44EsNfkeN0LmA3/LiGn1SUFwpF4yOru BjnV4XP6tc7zKJQspbeSPRdNV+kLff2cvqCyyGoktF0ddiUG9z/hwAUjVjGPgptIroaXepsp 4mNqNLa2EDkvq48dnLwwb2tNvBuy52pfex1NsnXEiFrrRGaUpWx3ypZqnGKF5NZtfh8uO+lf lKcQ+mtf4c3X9x9+iVkWxJGGUxAN5WtP7bSngLjnfGiERNH7BfmKumg/nrXbW12UC8EFpn9K w3sscaV+dFqg9VQNSAAGs1ZLcd0EH37VYsiUu/Bhz2SI22ro1GF47XczEtqrXmBD3SfC8/17 K7UXhW0Jlz4pKjMy8ofqIBo+AEeCHFmm+QrY0YB4JhMhiunCHIdZ/EoWXnc5kq4TgSpvH05W N3MUIfmISD0XDABaRelpdq+B0GQAesBPtq/LTssl69Rh+FaG6vYaIaNNA85i5u1Rtcn5O6iI NAavHb3O3BdB7l3EP0L6KXTbfhPn5vnK7Fhxaw5u8P3ChcaR74N0RSN2eaLuTPvS6nwqakAG YT5qa2ojq12pY4d3PuMo0JoJSw=
- Ironport-hdrordr: A9a23:x9c9DKHkg2eQ3aHGpLqE0ceALOsnbusQ8zAXPiFKOGVom6mj/f xG885rsCMc5AxhOk3I3OrwW5VoIkm8yXcW2/h0AV7KZmCP01dAbrsD0WKI+UyGJ8SRzJ866U 6iScRD4R/LYGSSQfyU3OBwKbgd/OU=
- Ironport-phdr: A9a23:ZTADnRJoKmdPEOSyyNmcuKZsWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFu7Mx3BSWAM3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmT owZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsip1u2+4ZLebgZHiDe/Yb55M Qm7oxjWusQKm4VpN7w/ygHOontGeuRWwX1nKFeOlBvi5cm+4YBu/T1It/0u68BPX6P6f78lT bNDFzQpL3o15MzwuhbdSwaE+2YRXX8XkhpMBAjF8Q36U5LsuSb0quZxxC+XNtDwQLspWzqt8 r1rRQfnhycJNTE38G/ZhM9tgqxFvB2svAZwz5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5umY YsOEeUBJ/xYoJfgrFYQqhu+GBOsBP/uyjBWm3/9wKo30/wgEQ7YxgwgBcwBvG7Io9XyKacSS /y1zKjWwjXedP5W1jL955LJchAlu/2DQbVwcc/IxEQpCgjKgUmep5b/MDOJyuQCrXKb7+x4W O+zlmIqrxx9rDexysowjoTHiY0bx1HY+ShkwIg4OMO0RU11bNCqE5Zcqz2WOohoT80tQ2xlu Tg2xLMatZOmcyUHzoksyRDYa/yCaYeI4xTjWf6QITd+nnJleaiwiwy88Ui6zOD3S8q60E5So yZbjtXBsmoB2h/T58SdVPdx40as1SyP2gzO7OxPPFo6mrDBK5E7x749jpoTvlrHHi/xgEj2i bWZdkQg+uSx8+TnYKjqqoaSN4J0lw3yKKsumsu4AeQ3NggBQXKX9vi71L3m5UH5QbNKgeMqk qTBrpzWOcAWqrS6DgJVyIov9QuzAja83NkYgHULNFdFdwiGj4jtNVHOOvf4DfKnjlS0kTdk2 erGPqf/DZnXMnfDl6rhfaxh605d1gUz0MtS551RCr4bIfLzXlX9u8DfDh88KwC0xf3oB81n1 owCQWKPHrOZMKTKvFOV/u4vOfWDZJcJuDbhLPgo/+LhjXggmVMEYaap2YYXZ2ujE/R9I0SZZ GLsjc0bHWcLuAo+Vu3qh0eYXT5dfXbhF547szo8EcetCZrJboGrmr2ImimhTbNMYWUTMlGBC 23lP66DRu0QaS+Papt5kzEeT7XnQIg8zw2vuRLSxL9uL+6S8Sod48GwnONp7vHewElhvQd/C N6QhjnlpwBcm2oJQ2Rzx6VjuQlmzU/F16FkgvteHNgV5vVTUw58O4SPh/diBYXUXQTMNsyMV E7gWs+vVCkwQ8grzpkFZFtnB9SvkzjM2iOrB/kekLnYTIcs/Pfk1mPqb914126A0aAgi1c8R c4aLWyrnLRysQPUGpTVkkiEv6mvfKUYmiXK8TTL1nKA6WdfVgM4SqDZRTYfa0/R+Mz+/V/HR qSyBK4PNwJAzYuaKPIPZICwy1pBQ/jnNZLVZGfZd36YIxGOy/vMaYPrfz5YxyDBEA0flBhV+ 3+aNA84DyPnomTEDTUoG0i9K0XrufJzrn+2VCpWh0mDclFh2ryp+xUUme3USvUd2agBsTsgr DM8FUi03tbfAd6N7wR7e6AUbdQ46VZBnWXX0m41doShIrp4ixgVdBlto0Ljyj14D4xBlY4hq 3ZrhAt+JKSE0U9QIiuC1MOVWPWfIW3z8RazLq/OjwuGgZDGp+FVsap+9gyw2WPhXlAv+Hhmz dRPhn6V55GRSREXTYq0SUEvsR5zu7DdZCA5oYLSz3xld6eu4Vqgk5okAvUozhG4cpJRKqSBQ UXqEsAAHcXoI+s3gUSoYw8sM+Vb9apyNMSjPajjuubjLKN7kTSqgH4Sqph831iW+mx3TfPSw 5cI3tmX2wKGU3H3i1Lr4aWV0chUIDoVGGS40y3tAoVcM7ZzcYg8AmCrO8Srx996ivYBQlZg/ UW4TxMD0c6tIl+JakDlmBZXzQIRqGCmni2xy3p1lSsop+yRxn6Gz+PnfRsBcmlFIQsqxU/tL JKugpYRW1WycwkkiTOq4E/7w+5Qo6E3I2TIQEhOdjT7NCk4Cvr25ufEOZcRrs5x+SxMNYb0K UiXULv8vwcX32v4Em1SySp6PzCmt5PlngBr3WeULXJ9tn3cKol7wRbS4sCZROYEhGJXAnklz 2OOWB7hZorMn53cjZrIv+GgWnj0U5RSdXKu1oacrG6g4nUsBxSjnve1k9mhEA4g0Ca92cM5M EeA5Bv6fITv0Ly3dOx9eUw9Tkf95tBgF8d1lZYqmJAdxFAVg5yU+TwMlmK5YrA5keruKWEAQ zIG2Yuf+AnowlduaHmO2pjlV3iA6sRkbti+JGgR32huiqICQLfR57tCkyxvp1O+pg+Eevlxk AAWzv424WIbieUE60I9iz+QCbcIEQxELDThwl6WusumovwdNwPNOfCgkVBzlte7APSerxFAD TznL4w6E3Y4790jYgmRliSisse+JIaWNZVJ6lWVi0uS0bQTcslq0KNU3Ww/fjus2B9tg+8j0 U4wg9fj5NLBcyM1u/jhSh9Aam+rOYVJpmCr3f4YxoHMh8iuBskzRW9NBceuFKPyVmpV7KSCV U7GESVg+CjHX+OFQEnHrh8h9iyHEoj3ZSjPdD9AkookFF/FYxYGyAEMAGdjwcV/T1H2gpSnK AAguFVzrhb5skcekLo5cUmiFD6F9EHwLW5rAJmHcEgMt18EuheTaJ3EqLo0RnAQ/4X9/lbUd CrBPFUOVjtPAgvdVjWBdvG47N3EuYB0H8KYKP3DKfWLoO1aDLKTwI63l5Bh53CKP9mOOX9rC 7s63FBCVDZ3AZaRnTJHUCERmy/XCqzT7B6h5i16qNy++/X3SUru44WIEb5bLdRo/Vi/n66CM +eagCsxJyxf09sAwnrByb5X21B36Wkmbz62DbEJrjLAVorVk65TSgYZMmZ9aZIO4KU70Q1Af 8Xcj5K917J1iOI0F0YQVVHlnZLMB4RCKGW8OVXbQUeTYe7edHubnoetOP36FOQD6Ycc/we9s juaDUL5azGKlj2yEguqLfkJlyaDehpXpIC6dB9pT2nlVtPvLBOhY7oVxXU7x6M5gnTSOCsSK z95JglVr7CK9y4eifJiAXBA42dNIuyNmiLf5O7dYMVz07MjEmFvmuRW7W5vgaNS9z1BTedpl TH6q9dvpxS+kLDKxGc+FhVJrTlPicSAukAoasC7vtFQHH3D+hwK92CZDR8H8sBkBtPYsKdV0 tHTlaj3JV+qHPrb+MIdA47fL8fVaRLJ1DLmHTfVCE0OSjv5bQk3ZmRYmfCWs2WX990098Gql 50JRbtWElcyE6FCYnk=
- Ironport-sdr: 64b808c5_DinbS21Nve/+vJaoXAwZsCO7uq3s5nI8eg3cMSbQNBBIChj 8XwnBlgx5+dofqGc1LqAGlTlT4lfew85RV1SaOA==
Hi.
AFAIK the only way to take a pattern as argument is to use tactic notations and the « simple_intropattern » argument type.
Pierre
Le mer. 19 juil. 2023 à 17:30, Chris Dams <chris.dams.nl AT gmail.com> a écrit :
Dear All,
I would like to be able to use a pattern as an argument to an Ltac
tactic. Is this somehow possible? At the moment I am running into:
Ltac program_data_destruct st ll glob H
:= destruct st as [ll glob|] eqn:H;
[fold mk_program_data in H |- * | fold mk_program_data_error in H |- *].
I would like to use a pattern instead of a complete term for st
because what I would like to pass as st can be quite large and I like
to fill in a few parameters to indicate which instance I want to
destruct but not all of them because that would be a bit too large.
E.g., I would like to do
program_data_destruct (set_pointer (mk_program_data _ _) _ _ _) ll' glob' H4.
but that runs into the error 'Cannot infer this placeholder of type
"program.stack program_global_type_info"'. Note that it would be quite
possible to pass the pattern term (set_pointer (mk_program_data _ _) _
_ _) as an argument to the destruct tactic, it is just the Ltac macro
that apparently forbids using this pattern term.
Is it possible to make this work somehow?
Kind Regards,
Chris
- [Coq-Club] Using patterns as arguments to Ltac tactics, Chris Dams, 07/19/2023
- Re: [Coq-Club] Using patterns as arguments to Ltac tactics, Pierre Courtieu, 07/19/2023
- Re: [Coq-Club] Using patterns as arguments to Ltac tactics, Chris Dams, 07/20/2023
- Re: [Coq-Club] Using patterns as arguments to Ltac tactics, Gaëtan Gilbert, 07/20/2023
- Re: [Coq-Club] Using patterns as arguments to Ltac tactics, Chris Dams, 07/21/2023
- Re: [Coq-Club] Using patterns as arguments to Ltac tactics, Pierre Courtieu, 07/19/2023
Archive powered by MHonArc 2.6.19+.