Skip to Content.
Sympa Menu

coq-club - [Coq-Club] assert that the output of Print Assumptions is a subset of

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] assert that the output of Print Assumptions is a subset of


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] assert that the output of Print Assumptions is a subset of
  • Date: Tue, 1 Aug 2023 13:08:51 -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:ZnzJeK++ElTIUdkIl7y4DrUDVnqTJUtcMsCJ2f8bNWPcYEJGY0x3x mVKCG7XPv2MM2XzLtoiao3noRlUsJ6AnIRmSQJt+3xEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPymYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWYtWo4ow/jb8kg37Kyr4GpwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TExM03Jl4kIosj+rxeJ00Xy KYiN24vV0XW7w626OrTpuhEg80iKIz0OdpatCw4iz7eCvkiTNbIRKCiCd1whm9hwJATW6+EN 4xEMVKDbzyYC/FLEl4dCJMlnOqrwHD5ejtU7lOUuaUf7G3azQg327/oWDbQUoXTFJUIwx/F+ Aoq+UzYJioYaP2akQOhrDH9o/TshT6rX6g7QejQGvlC2QXPnAT/EiY+Xlyi5PK9l0SWQMNaM 0VS+yw0rKF0+lbDczXmdxixoXrBoRtFHtQNS6s17waCzqeS6AGcboQZctJfQNse7eUpVyMs7 V/TtvXFXAE1iqLLa0vIo994sgiOESQSKGYDYwoNQg0E/8TvrekPYvTnHocL/Emd3oydJN3g/ 9yZhHNh2OhL3Kbnw43+rA+X2Wv9znTcZldtvl2/Y46z0u9uiGeYi2GA7FHa6bNfKd/cQATZ+ ncDnMea4aYFCpTleM2xrAclTOrBCxWtamW0bbtT838JqW/FF5mLI9s43d2GDB01WvvogBewC KMphStf5YVIIFyhZrJtboS6BqwClPaxTYS/BqqPNoAROPCdkTNrGgk+NCZ8OEi9wSARfV0XZ P93jO72XStEVfo5pNZIb75GieZ6rszB+Y8jbcmjk07PPUu2a3mSRrMIWGZinchohJ5oVD79q o4FX+PTk0s3eLSnPkH/r9RPRXhUdiNTLc6t+6RqmhureFUO9JcJUK+Pn9vMuuVNw8xoqws/1 izjAx4HlASm3xUq62yiMxheVV8mZr4nxVpTAMDmFQ/AN6ELMN33vpQMPYA6Z6cm/+FFxPt5B atNMcaZD/gFDnyN9z0BZNOv5MZvZTa6tzKoZiCFWTkYe4I/Zgrr/tS/QBDj2hNTBQWKtOw/g Yaa6CXlfbQ5ST9PMuPqedO07lbovXEiiON4BETJBd9IeXTTyothKg2vr/puI8gzNgnPnGOK8 zmnWDIz+O/H+d4z+vb0mJHe/puIEvR/LGVeDWL0/ba7DgiE32uBkKtrcveEQiDZb0zwoJ6dX ORyy+ruFdE2h3NIjtZMKKlqxqcA+Nffnb9W4QB6FnHtbV7wKLdfDlSZ/MtI7Ith+6R4vFaoZ 0ex5dVqA7WFF8f7Glo3JgB+TOCi1+kRqwbC/8YOP0T2yy9mzoWpCXwIEUG3txVcC79pPKcO4 +Qr4pcW4jPirCsaCI+NiyQM+lmcKnAFbb4ciagbJ43V2y4L0VBJZKLOBhDmuK+vb8p+CWh0A zu2qpebuZFi6BvsT34BG0LJ/9JhvrUVmRUTzFY9N1WDwdXEofks3Sxuyzc8TyUL7xBLz9NMP nNPMmtrL56v5BZtvtBIBEq3KjFCBTqY203/8EQIn2vnVHuVVnTBAWk+GOSV9mUbzj54Uh1E2 oqHkUDJfC3Pfs7j+gcTA2tetO3FX9h90ibgifKXNZ2JMLdiaAW0n5L0Q3QDriXWJP8YhWrFg LJP1/lxY6iqDhwgifQ3JKfC3ItBVS3eAnJJRMxg26Y7HWv8XjWW8hrWImCTfvJ9HdD7wXWaO edPeP0WDw+f0RyQpA81HaQPer94vMA47eo4J4/EGzQ0jKu9nBFI7rTgrjPzlU06ceVIyMwdE L7cRxiGM26XhEZXpVPzkdl5CjK4TOQANSLB37GT0eQWFpg8nvlmXmMs35CV4XiEEgtV0CiFn QHEZp2Mluxr9ptxrtG9DoRCGASGBtfhX8uY8A2IkopvbPGeFezspg8qul3cEAAOBoQoWvNzj qWrjNHs+VHs5ZIabjj8oIaQMIVs/uCwbfpzHuOsC0cChgqEesvnwyVbylCCMZYTze9svJi2d TW3eO6bVIAwSdxC4FZ3diIHMRIWK5qvX5favSnn8si9UEkM4zfmcuGi22TiN1xAVykyPJb7N A/4ltCu6v1cr6VOHBU0PO5nMbApPG7cXbYaSPOpuQm6FmWIhnawionmnzck6hDJDSCKLp+rq 9aNDB3zbw+7t6z03clU+d469AEeCHFmx/I8ZAQB8tpxkCq3F3MCMf9bC5gdF5VIiWbn4fkUv t0WgLcKUk0RnAiocCkQJPzmVwabQ/MLY5L3e2Rv8ESTZCO7QoiHBdONM8umD2heIlPeICOPc LnyOUEc+jC+x5hoQaAY4fnTbSJP2KbB3nxRkaziu5WaPvvdaInmEFRuGQNMUWrMFMSleIAn4 4QqbTgsfXxXgnId3Sqtl7C51f3ZUP7SI+0UUBqy
  • Ironport-hdrordr: A9a23:FG/nBaNGJ36uGcBcTsyjsMiBIKoaSvp037BL7TEXdfUxSKalfq +V7ZcmPHPP6Ar5O0tApTnjAtjjfZq0z/ccirX5Vo3SOTUO1lHYSL2KLrGP/9QjIUDDHyJmup uIupIRNOHN
  • Ironport-phdr: A9a23:t89bTRe9bEe8r3gQpSPttmxylGM+NdTLVj580XLHo4xHfqnrxZn+J kuXvawr0AWXG9qFoKsc16L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNYghEnjiwbLJ9I BmrsQncudQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2U bJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5 KptVRTmijoINyQh/W7YisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8a pMCAvYaMuZYron9vFsOogW9BQKxGO7vzCVHhnnr0qYn1OkuCxrJ3AwhH9IVsHTbstb1OL0IX uCz1qbIyyjMY+lX2Tf89IjIfQssof6JXb1qcMrRzVMjGB/CjlWVsIHoOS6e2esRvWaB9eVgS f6vhHA9qwF3ujWi2Mcih5fUi48axV7J6Dt1zYgrKdC7VEN2b96qHIVfuiyeNYZ6X8EvTnxot Sg6yLALupy2cDQUxJg5xBPSaPKKfo6V6RztU+aRJC13hHNjeL+nmxmy9lKgyuviWcmw1FZGt DRKncTRtn0Lyhfd6dCHR+Nj8ku93TuDzQPe5+FeLUwpi6bWKIQtz74smpcVrE/NBDX5mF/sg 6+Tbkgk+van6+DgYrj+o5+TLY50igXnPqUgn8yzHP00MgYOUmSH4+i827rj/Ur2QLVOkPI6i LXWsJffJcgDp665BRFa0po75hqhEzur1M4UkHoHIV5fZR6LkYvkN0vOLfzkFfu/hk6jkDZvx /DIJL3hBZDNI2DZn7j6fbZ96lVcyAotwtBc/Z5bELcBL+j1WkDsrtDYDx45MxC7w+v8B9V90 5kRWWOLAqODLKzStlqI6vopI+aXfIAVoiryK+A55/7yin80gUIRcbGz3ZQLcHC4AuhmI0KBb HXwhdcBCH4GsRY6TOz3k1KPSiVTZna3X6Ik/D43EoOmDYHZRoCsmrONxim7HocFLlxBX1uLC DLjc5iOE6MHbzvXKct8mBQFU6KgQskvz0f9mhX9zu9OJOrV4S0VttrK0tFz66WHnBsy9Cd0A sfb2meESW0yn2IUSBc52al+pQp2zVLVgvswuOBRCdEGv6ABaQw9L5OJl4SSavj3UwPFJJKST Uq+B8+hCnc3R84wxNkHZwB8Hc+jh1bNxXniGKcbwpqMApF86afAxz7pPc8ownzG1bIhglpgS 81GM2Hgh69j+CDcAofIlwOSkKP5Pb8E0nv1/XyYhXGLoFkeVQdxVavfWnVKb0HWrM/560CER rmnD7hhMwpdxuaNL6JLbpviilAVDOz7NoH4ZGS803y1GQ7Oxr6Ia9/yfH4B2SzGFEUeuwUa/ HLDKg1nQyn8+yTRCzthEV+paETpmQVngFW8SEJ8jwSDbkk7kqGw5gZQn/uXDfUawrMDvi4l7 TRyBle0mdzMWZKGoEJ6caNQbMlYgh8P3H/FtwF7Ip2rLrxzzl8YfQNtukry1hJxQoxemMkup XkuwUJ8M6WdmF9GcjqZ29j3NNi1YiH79hCucK7b2RfX1t+Q9uEO6eg3g1rmtQCtUEEl9jQv0 tVY1Wed+oSfFBAbAveTGg488xl3oa2fYzFovduFky0xd/Du4nmfg4FMZqNt0BurctZBPbnRE QbzF5dfHM2yMKkwnFPvaBsYPedU/apyPsW8dvLA1rT4WYQo1D+gk2lD55hwl0yW8C8pAOfC3 5cew/ybmAKBXjHwylagrs/floVNZDVUFW26g3uBZsYZduhpcIAHBH37acS9xtRlh5PuHXde/ VivQVIHxMCBdh+bbli71gpVnxdywzTviW6zyDp6lCssp6yU0XnVwujsQxEAP3ZCWGhoiVqEz ZGct9kBRwDoagEokEHg/kPm3+1Bo685KWDPQEBOdiywLmd4U6L2uKDQK8JI7Zopt21QXoHeK RiTQL78uBsX0GXqGWJYyHY6di2lkpr8lh1+zmmaKT5/oWHYdsd52RrErIaEFLgBg3xfHnk+1 GGfD0PZXZHh5diOkpbfru2yH3msUJFea2ijzI+Nsje6+Xw/BBS+m/6pndi0WQM+0CL9y5xrT XCS9Ee6MtStjv7qd78/LSwKTBfm5sF3G59ziN41jZAUgz0Bg4mNuGAAmiH1OMla3qT3aDwMQ yQKypjb+luAugUrI3SXyob+TnjYzNFmYozwa2kW2zk94sMMAaGd6rACnCpprXK3qAvQZb52m TJXmp5MoDYKxvoEvgYg1HDXC7oSHFJYMC+qnhKB6dz4raRLa06gdLGx0Ax1mtXrX9Tg6klMH X3+fJklByp56M5yZUnN3HPE4YbhYNDMbNgXu07cg1LaguNSMp50iusSiH8tJzfmpXN8gb1e7 1QmzdSgsYOAMWko4K+pHksSKGjuf81KsjD10fQFw4DPjtjpRMk+XG1MBsegTOr0QmxO8668b EDXTmV68jDCSN+9VUee8Bs08SyJSsjxcSnRfD5DlZ1jXEXPehIZ2lxFGmVi2MZ+TFjixdS9I hgjoGlNoAep8F0Ujbs4Unu3GmbH+FX3NnFtEsXZdFwOqVgcr0bNbZ7HtrI1Rn4HuM3n9EvXc ySaf1gaVD5SHBXVWxa7eOHpvIelkaDQB/LifaGWMPPe9KoHDafOndX2jcNn52rebJzReCQyS aRqgAwbGikoU8XBx2dVEnJRzXmcKZXB4k/7o3wSzIj35v3vXEiHCZKnLbxUPJ0v/hm3hf3GL OuMnGNjLj0e0JoQxHjOwbxZ3VgIiigoeSP/WbIH/TXASq7dgMo1R1YSdj9zOc1U7qk9whgFO MjVjcnw36J5ifh9AklMVFjokMWkLcIQJGT1OFTCDUeNfLOIQF+Di9nwer+5QKZMgf98shSxv XOEFhamMGnb0TbuUB+rPKdHiyTadB1StYehcwp8XGjuSNW1D3/zeNRzjDAw3fg1niaQbT9aY WU6Khkd6ODIvkY6yr1lFmdM72RoN7yBkiedtazDL4oO9OFsCWJynv5b53Izz/1U6jtFTbp7g ni3zJYmrle4n+2I0jciXgBJr2MBjYiLvF5iNKaf/59JX3qC/RMR4k2fDh0Lo51uDdil6MUyg pDf0bn+LjtP6Yee5cwHG83dM96KKlIkOBvtXSHRVU4LEGbtOmbYiEhQ1vqV8zfGy/py4oipk 50IRLhBUVUzHf5PEUVpEusJJ5JvVy8lm7qW5CbpzX+3rR2UW8AD+56aDrSdBvLgLDvfhr5BN UNgKVzQIoEaN4m90EtnOAASdGHiFE/ZXNQLqSpkPFdcnQ==
  • Ironport-sdr: 64c93c49_pcEcth1cMJ63q4Abz6QtABYOVLvGi3/nKQBkc6mjwz9TqhV RDBRJj5oNmGce5oILjLAjKFdzxSWsWEwqucn8Xg==

Is there some Coq vernacular to assert that the output of Print Assumptions on a lemma is a subset of a set (specified as a list) of fully qualified names?
If not, what are other ways people ensure that this doesn't grow inadvertently?



  • [Coq-Club] assert that the output of Print Assumptions is a subset of, Abhishek Anand, 08/01/2023

Archive powered by MHonArc 2.6.19+.

Top of Page