Skip to Content.
Sympa Menu

coq-club - [Coq-Club] match on multiple goals simultaneously

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] match on multiple goals simultaneously


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] match on multiple goals simultaneously
  • Date: Thu, 28 Sep 2023 10:48:02 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f50.google.com
  • Ironport-data: A9a23:wDeo9Kj6SiG8On4IcBg1iBr3X161FBUKZh0ujC45NGQN5FlHY01je htvDTzXOf+KNmegf952PYq38EpVscKBzNU3T1Nk+HtjQX9jpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqieUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYqdDpPg06/gEk35q+q6WlI5gZWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGKU1tG6QS2LZLM05P0 uUkIiExMBDSmLfjqF67YrEEasULKcDqOMYAvyglw2yBS/khRp/HTuPB4towMDUY3JgfW6aDI ZNDOXwyNHwsYDUXUrsTIJs0nOazhnT8NTReoVSZ46s2/2f7wwl40byrO93QEjCPbZwPzhrH+ jmWrgwVBDkXbv+mlhnbzkjxj+bBwj/CeYI3EbeRo6sCbFq7gzZ75ActfVC8uLyyjlO0c8lOL lQdvCsot6k7skKxJuQRRDW9qX+A+wEZAp9eTrV85waKxa7ZpQ2eAwDoUwJ8VTDvj+duLRRC6 7NDt4qB6eVH4ebNG0GOvKyZty2zMiUzJGoPL31MBwgc7tWp5Ml5ghvTR5wxWOS4n//kKwHWm jqqlSkZg6lMrMgp067gw0vLrQjxrbf0Tyk0xD7tYESb0i1DarWIXbeYsWrg0a4YLaKybEWwg 3wfqs3PsMEMFc6skQKOcsUsHZaoxfCPDxPEi3UyHZN7rzWJ0FygdLB2/ztRChpIMMEFWDmxe 27Vm1pby6FyNUuQT51cQtyOGeVz6oP/B/HJa+vyUuNeRrRQKCqW4zBIZ2OL+mLmzXgXjqA0P KmEffaWDXo1DbptyBy0Tbw/1YAH6z8fx2TBY4LS1DWijKSjYUCKRYc/MFehav4z6IWGql739 /ddL8679AVNYtbhYyX48Z8hEn5SFCIVXavJks1wcvKPBiFEG2t7Uv/Y/u4HSrxfxq9Qkr/Fw 2G5Vkpm02HAvHzgKzvbTlB4abjqY4RzkmJjAwwoImST+iYCZaSB0f4hUqUZLJcb8N5t9/pWd 8U+Wt6hB61PQwvX+j5GYpjaqpdjRSuRhgmPHnSEZTQjTqFkXCjM3MHuRSr01Sw0FiHsn9APk 76h8QL6QJQ4WAVpCvjNWs+v11+cuXs8mvp4ekn1fv1/XVrKy5czDQDcldo1LNMoBTSZ4wCFx iCEBRs8jsvckb8fqdXmq/iNkNa0LrFYAEFfIVj+0Z+3Eiv/pU+I3o5KVbezTwD3DW/b1v2rW rRI8qvaLvYCoVdttrh8GZZNyYYVxYPmh51e/zReMET7VXaZIZI+HSDexuhKjLNH+ZFBswjvW k6vxMhTCY/UBOzbSmwuNCgXRcXd88FMgTTDz+UHEGOj7g9Nwbe3e0FzPR6NtS9jEIVIIL4Vm ecPhONG6iiUqAYbDdKdvyUFq0WONiMhVoskhLE7AajqqBYa9VVZRazQFgrNuZSpV/xRABN7P A3OlK7mgpJCzHHjaFs2L2DGhsBGtKQNuTdL7V4MHEuIkdz7nc0K3AVd3DA0bwZNxDBV+rhXF kkyEGMtPoSI3TNjpPYbblCWAwsbWSGooB3g+WUGhEjybheOVFWUCEYfJOzU3kQS01wETwhh5 LvClVrUC2f7TvrQgBk3d1Vu8cH4bNpL8QbHpsCrMuKFE7Q+YhvnmqWeXnUJmTS2HfIOgFD7m scy8NZScaHbMQsik58/AaSe1pUST0mKGjUTC7UptqYEBnrVdzyOyCCDYRL5MN9EI/vRt1S0E YpyL8ZITA6zzzuKsitdP6MXPrtoh7Q80bLuoF8wybIu6NNzbwaFsa48MgD7jW4vBspryIMzd 9uXeDWFHWidw3BTngchaSWC1nWQObE5iM/UhYhZM9nl07oMtehtdQc51b7cU7C9Ll585xzN1 O/cT/a+8gGhoLiAW6PjF6xCA0O/LtabuCFkNuysm4wmUO4j+vsie+/YRpcL8uiW0XYstwxLq Imw
  • Ironport-hdrordr: A9a23:zmQ7H63Bhrmq2AY8KBZKqwqjBL8kLtp133Aq2lEZdPU1SL3+qy nKpp4mPHDP+VUssR0b+exoW5PgfZq/z+8W3WB5B97LNzUO01HYSb2Kg7GSpwEI2BeTygee78 pdmmRFZ+EYxGIVsfrH
  • Ironport-phdr: A9a23:lOk+5BN3O1SI4efca/kl6nZiBBdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv6Ur1AeCAdSTq6odzbaM7ea4AS1IyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexf7B/I A+qoQnNucUbjo9vIbs1xhfVv3dEYetbyX1pKF6Jgxrw+sK894N//ipNvP4s69ROWrjgcaQiS rxYAjUmM2Qr68DuqBLOUwiB6GYCX2sPihZHDBTL4x/8Xpfqryv1rfF91zWAPc33Vr87RzKv5 Lp2RRDyiScHMzk58HzLisF1kalWrg6tqwB5zoXJZoyeKfhwcb7Hfd4CSmVPXshfWS9cDI2ic 4QCFPAOMfpCooTnu1cCsRmzCA+xD+3v0D9IgXr20LUm3us6EQHG3RcgH9IQv3TXsd74KKESX vqzzKbV0D7OaOlZ1iz96IjJaRAhoe+DXbFqfcXLz0kgDQXFgUiKpYzkPjOVyusNvnOU7+plT +2vimonpxttrTiow8chk4/EjZ8axV7Y7yt22po1JcGmR05hZ96pCIVduSGEOoZrTc4sTHxlt Dg0x7EYupO2YCYHxpQ5yxPQb/GKcZWE7xD+WeuRITl1hnFodbCjixqs70Stye7xW8ey3V1Xo CRFldzMuWoM1xzV8sWIVvx9/l2n2TmR0wDT7vtILl4pmqrGLZMq370+loILvEjdAiP7nF/6g ayWe0k+5+Sk9efqbq/mq5OAMYJ/lxvwPb40msOlBOQ1KggOUHaf+eS7zLDj+Ff2QLROjvEvn KjZtY3WKd0VpqO5HwNZyIkj6xG4Dzep1NQXg2MLI05CeBKCl4TpOlfOL+7kDfqnnVigjDNmy +rFM7DhGJnBM2bPnbT7cbt990JQ0A8zwspe55JQBLEBOvXzWkrpudPCFRA5Mw20w/3nCNpj1 YMSQ3iAAqmDP6PUrFCE/OMvI+iQZI8aozv9JP0l6OTvjX89g1MSYa6p3Z4PZHC+BftpO1+Zb mb0gtcdDWcKuRIzQPHyhF2YTTFTf2qyX7475jwjFI2mCp7DSpmxj7yFwSe0BYZbZntGC1CJC XfnbZ+IW/YKaCKII89uiCYIVba7S9xp6Rb7vwjjjrFjM+CcriYfrNfo0MV/z+zVjxA7szJuW ZezyWaIGkh+nmITRzI1lIl5qEpxggOK26h5mPxVFppa4fpPXkE7NILT5+N/AtH2HAnGe4HaG x6dXty6DGRpHZoKyNgUbhMlcz3DphXK3i7wRqQQi6TOHps/tKTVw3n2Ic95jXfAzqgoyVc8E YNULWPzoKl5+kDIApLR1V2DnvOjf6Qdxy7A9yGKy2OIsAdZURJ/earAVHEbIEDRqIex/VvMG oenEq9vKQ5d0YiHI6pOZMfuiABPTvfiI9TTYCS4nW62CVCJx6+DRIXvcmQZmi7aDRtMiBgdq FCBMwV2HSK9uyTeAThpQEroeF/p+PJipWmTS0Y1y0SVahQk2eftvBESgvOYRrUY2bdsVD4Jj TJyER792tvXD4DFvA99ZOBGZth75l5b1GXfvgg7P5q6LqkkiERMOwJw91jj0Rl6EOAi2YAjs W8qwQxuKKmZzEIJdjWW2or1M6HWLW+69Q6maqrf0FXTmNiM/aJH5PM9olTl9Aancyhqu3xt0 9hO03afoJzMBQweF5PwTkkf+B1zprWcaS44psvV2XBqLaioo2rawdt6YYltgh2kftpZLOaFD FqoS5xcV5XocbZ63QXxPXdmdKhI+aU5Pt2rba6D0a+vZqN7mS6+yH5A68Z7216N8Cx1TqjJ2 YwEyreWxFjiNX+0gVG/v8TwgY0BaysVGz/1wCLkBZVRa640dIACD2voIsyryf1xgpfsXzhT8 1vpVDZkkIe5PAGfaVDwx1ga3E4XoGenlCj+xjp9lT1vr6uD0wTBxu3jcFwMPWsBFwwAxR/8Z IOzid4dRk2haQMkwQCk6UjNzK9evK1jLmPXTC+kZgDOJnp5Guu1v7uGOYtU7Y8w9D9QW6K6a EybTbj0p10b1TniFi1Q3mJzezavs5T/1xt07QDVZH95rHvCecxzgx7Z7drQA/9QwjUuSyxxi D2RDV+5d9Wk5tSbkZ7fv/v2DTrwEM0ON3CxncXd7GOy/ggISVWnkuq2m8H7HARyyiL929RwF G3JoBv6foj3xvG/OONjcFNvAQy04M57F4di14oo0ctIiD5K29PMpypBzD+gVLcTkbjzZ3cMW zMRltvc4Qy/nVZmMmrM3YXyEHOU3spmYdC+JGIQwCM0qc5QW8L2pPRJmzV4pl2goEffe/94y 30Uw/sv834XgKcAvgMrwmOcA6wdNUZdNC3o0R+P6prtyccfLHbqarW22EdkyJqoBrGDuQFRW zDwfJ4kEWlx79lwGF3J2Xz3rIrjfZODCLBb/g3RmBDGge9PLZs3nfdfnitrN1X2ung9wvI6h xhjjtmq+ZKKIGJ38OelEwZVY3frMtgL9Gin3sM81o6GmpqiFZJ7FnAXUYv0GLi2RSkKu62vN h7SQmZh7C7KQfyFQVDZsAA88zrOC8z5aS3RfiJCi4w8HF/FYxUO5WJcFDQiwsxnSEbznJanK AEhoWpJrl/g9kkSlKQya0i5Aj+Z/EDyMn81UMTNc0AQt10EvhaPd5TZt7IWfWkQ/4X9/lPRb DXBOkIQSzlOAxLMBki/bOD2tZ+ZrLfeVqzmaKGXKbSW9b4HCKzOnMPzlNMgp3HVaKDtdjFjF 6FpgBISGyAkXZ2Dy3NXDHVI3yPVM5zB/Un6p30x95HltqysAVOn5JPTWeELb5M1oEHw2v3Fb 6nJ1UMbYX5O35cIjxck0ZA521gfw2FrfjipS/EbsDLVCbjXkelRBgIabCV6MI1J6bg9109DI 5yTjNS9zbN+gvMvbjUNHVX8hsGkY9ALKGChJRvGAkiMLrGPOTzMxYn+f6q9TbRaiOgcuQe3v H6XFErqPzLLkDeMNVjnKeZXkCSSJwBToqm4exdpTHfmFZfoN0X9P9hwgjk7h7YzgzKCNGIRN yR9b1IYrrCU6nA94L03EGhA43x5aOicznzBvq+Id9BP66stX3wn8oASqG43wLZU8ixeEfl8m S+I68Vrv0njiO6EjDxuTBtJrD9PwoONp0Rrf6vDpfwiET7J+gwA6WKIBlEEvdxgX5fmsaBR0 djCl+T6Lj5E/5TV/NcTL8fRIcODdnEmNFC6fVycRBtAVjOtOWzF0gZFl+qO83SOspUggp3lm Z5LVboCEVJoTrUVDUNqGNFEK5ByFGBB8/bTnIsD4nywqwPUTcNRs8XcV/6cNv7oLS6QkbhOY xZgKVbQIoEaN4m90EtnOAESdGXiHkPRWZVSp3QkYFJs5kpK93d6Qys43Ee3MmtFD1ccEPe1m lg9jQ4sOIwQ
  • Ironport-sdr: 6515924f_ak/bHiJc2HlLj8TX57cPYJbgg9Bl8tl1+19+QYGvh80Avxm xf2HkRjxkmLA9jyQMYPVOE7Zxad1M8z/P9MA30w==

often, I have an evar shared between 2 goals and to correctly determine the right value of the 
evar, I need info from both goals.
is there some way to match on multiple goals like:
match goal1 with
  [H1: pat1 ?X |- C1] => 
        match goal2 with 
          [H2: pat2 ?Y |- C2] => unify shared_evar (f C1 C2 X Y)
         end
end




Archive powered by MHonArc 2.6.19+.

Top of Page