coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Definition as opaque as Qed
- Date: Thu, 2 Jun 2022 06:19:33 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f46.google.com
- Ironport-data: A9a23:Be5JwKNsWjRGySnvrR2akcFynXyQoLVcMsEvi/4bfWQNrUpxgWBUm DdNWWiAPP6KY2Wjct51Pozk8UoD75LVx9JkT3M5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8kk/vgqoPUUIYoAAgoLeNfYHpn2EsLd9IR2NYy24DnW1rV5 bsenuWGULOb824sWo4rw/nbwP9flKyaVOQw4zTSzdgS1LPvvyF94KA3fcldHFOkKmVgJdNWc s6YpF2PEsw1yD92Yj+tuu6TnkTn2dc+NyDW4pZdc/DKbhSvOkXe345jXMfwZ3u7hB2LhPBJ5 IRx9qWUYjkJEKnjnvQsQUNxRnQW0a1uoNcrIFC6uM2XikDKKj7in6soA0YxMokVvO1wBAmi9 9RCcGFLPk3F3brmhu7lIgVvrpxLwM3DOZ4ct2pg0TDGBOwnB5HCQrnPzdBd1TY0wMtJGJ4yY uJANGQ/MUqYMnWjPH9KJ5AmjL60j0DnfhZ690OJlZcFz1HMmVkZPL/FaYKJILRmX/59lUGB4 2nC4m7RGQAfLNXZyDyf83vqiPWnoM/gcIcbFbn9+/IzxVPPmCocDxoZUVb9qv684qKjZz5BA 04P2hIC/JRxzWiAcPnTWzK+sE+W5DdJDrK8DNYGwA2Kz6PV5SOQCW4FUiNNZbQaWCkeFWxCO rihz4OBONB/jFGGYSnCqerM/FteLQBQfDBSP3ZVJecQy4C7+Nlbs/7Zcjp0/EeIYjDdHDjxx 3WHoHF7ielNy8EM0Kq/8BbMhDfESnn1ouwdtl+/soGNtFsRiGuZi2qAtwSzARFoctrxc7V5l CJY8/VyFchXZX13qASDQf8WAJai7OufPTvXjDZHRsd8q231qyT4Jd4MsFmSwXuF1O5UKVcFh 2eD6WtsCGN7YRNGkIcsPtjhVJ5wpUQePYW4Cqu8giVyjmhZLVfbpkmClGaf2GfilEVErE3ME cbzTCpYNl5DUf4P5GPuGY81iOZ3rghjmz67bc2kl3yPjOvGDFbIGOxtGAbfPogRsvnYyC2Lq I03H5XRm31ivBjWOHa/HXg7dgBUcxDWxPne96RqSwJ0ClM2Rjt6W6WPnu1Jlk4Mt/09q9okN 0qVAidwoGcTT1WeQelTQnw8Or7pQ7hlqnc3YX4lMVqyiiosZI+u6OEUcJ5uJesr8+lqzPhVS fgZepXYUq4fFGifozlNP4PgqIFCdQiwgV3cMiegZg85dcEySgHM/OjiYQaypjIFCTC6tJdlr rD5jlHbTJMPSh5MFsHTbP7znVq9sWJMyu13VkrMZNJUfRy0ooRtLiXwiN4xIt0NeU2TnGvEi 17ODE5B9+fXooIz/N3Yvoy+rt+kQ7lkA05XP2jH9rLpZyTX+2yUx4UfAuuFeDbqUnytpPeva OBT+PHLMPMdmWFMvYchQa1gyrgz5oe2qrJXklZkEXHMYwj5A79sOCPdj8xGt6kIy7MA/AXqB ASA/d5VPbjPM8TgSQZDKA0gZ+WF9PcVhjiCsqhvcRuivHd6rOidTEFfHxiQkygBfrF7B4Uon LU6s8kM5g3j1xcnboScgiZP+zjeJ3AMSf985JQTAYuuhwZyj18eP9rTDSj55JzJYNJJaxF4L jiRjavEprJd2kuSLCZpRCaVhbJQ1cYUpRRH7F4ePFDVyNDLsfk6gU9K+jMtQwUJkxhK3oqf4 ISw25GZ+ElPw9tpuCSHd2WlGgUECRHAv0KtlR0Gk2rWS0TuXWvIRIH41SBh42hBm1+wvBACl F1b9IoheTnvdcD1mCA1XCaJbtT9GMdp+FSqdN+PRqy48lpTXdYhqqCrbGsM7RDgBKvdQaEBS fZCpI5NVEEwCcLcT2DXxWVXOXT8hS1o/FB/fMw=
- Ironport-hdrordr: A9a23:iHBBIq1X1zm0lYJIwkTDMwqjBIskLtp133Aq2lEZdPU1SL3gqy nKpp4mPHDP+VMssR0b6LK90ey7MBDhHP1OgLX5X43SODUO0VHAROpfBMnZowEIcBeOkdK1u5 0QFZSWy+edMbG5t6vHCcWDfOrICePozJyV
- Ironport-phdr: A9a23:Wg1nphPZTYwrcptlTAcl6na+BxdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv64r3QaCDdWTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7ye6/94fXbglVizawYrB/J wiqoAvMscUbnZFsIbsrxBvTpXtIdeVWxWd2Kl+Wgh3x+MS+8oN9/ipJo/4u+NJOXqv8f6QjU LxXFy8mPHwv5M3qrhbMUw2C7WYBX2oMkxpIBw/F7AzmXpr0ryD3uPZx1DWcMMbrS70/RDas4 LpxSBLwhygHOTw2/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6ka osPEukBMvhDr4n9ulAOsRq+BAe2C+P1yz9Dm3j73agn0+QiDw7GxwwgH84PsHXattr1LqYSX fq0zKnJzDXDc/ZW1Czy6IjNaB8hoPWMUahsfsrWzEkiDgXIhUifpoL5JT2azPgNs3SF4Op6U +Kik3MqpgBtrzWsx8oihYfHiI0Vx13Y9ih13oc4K9OmRUN1fNKpDplduj2ZOoV4Qs4vQ29lt To4x7ACtpC1fDUGxpQhyhXCZfKHdI2I7QjiVOaXOTp4i3NleK6/hxav6kes0PHzVs6x0FpSr ypFlMPMtnEX2BDJ5MiHUP1w9Vqi1zaXzw3f9P1ILEQumafYK5Mt2KA8moYQvEjZESL7mUP7h 7KMeEo+4Oin8eHnb63mppCCM490jRnzMqE0lcy+BeQ0KxYBUHWG9eil2r3u8kz0TK9Fjv0xl anZv5TaKtoBqqGlBA9V154v6xe5Dzi4zNQVhWcLIE5BdR6djIXkO0vCLO7kAfq8mVihnzZmy +jDPrL7A5XNKnbDkK3mfbZ480NczRczzdNB6JJPCrEBPPPzW0Hru9zCDx81KQ20w+fmCNVh0 4MTQm2PAqqDP6PTtV+E/P4gI+6JZIMNvjbyMOAq5+Tygn8hhV8dYa6p0IMKZHygBPRpP12ZY WbwgtcGCWoFog0+TPXzhFKeVT5Tem29Urkn5jA7DYKmFZ3MSpqsgLyHxie7H4dZanpIClCWQ j/UcNCPXO5JYyaPKOdglCYFXP6vUdwPzxar4QrnyLd8LqLI+zIRr5OrgN1o5ODIlQ0z6jVuD oKc0mCRSkl7m2oJQ3k926Up8h818UuKzaUt268QLtdU/f4cCm/SVLbZxu1+UJXpXx7ZO8yOU BCgS8mnBjc4SpQwxcUPagBzAYbqlQjNigytBbJdjLmXHNos6KuJ2mXyKt1913fZ3bMgyVgnQ 9dKHWKjj697sQPUAt2BiF2Xwp6jbr9UxyvR7CGGxGuKsltfVVt1TKbIRnADZ1Tft9W/50LDU 7qGBrEuMw8HwsmHeeNRctO8q1JASb/4PcjGJWK8n2DlHRGT2raFd5bnYU0Y1STZTUUIykUdo SjAOg85CSOs5WnZCVSCDHrJZEXhual7oXK/FQovyh2SKlZmz/yz8wIUgvqVT7US2KgFsWEvs Wc8GlH1xN/QB9eawmgpNKxBfdMw5ktG3mPFpkR8OJKnNaVrml8ZdUx+oUrv0xx9DogIn9Itq Tsmyw97KKTQ110kFXvQ2I3zN6bXNmjt9QquLa/X203b+NmT86YLrv8/rhSrvQ2kEFYj72Qyy 8NcgB7+rt3BCAsfV460U15irUAr4eGHJHNlt8WIiy4JU+H8qDLJ1tM3CfFwzx+he4waK6aYD ErpFNVcAcGyKessklzvbxQePekU+rRnWqHuP/aAxqOvO/5t2Ty8imESqoVg0U+X9zZ9VefS3 tAEwvCE2yOIUj79iBGqtcW9yuUmLXkCW3GyzyTpHtsbY7BxcJ0LFWaxKte2gNR/hoLoc3Fd/ V+nQVgB3YX6HHjaJ0y41gpW20MNpHWhkibt1D14nQYiqa+H1TDPyeDvHPYeElZCX3IqzVLlI IzvyssfQFDtdA8x0h2s+Uf9waFf4qV5NWjaB0lSLWD6KGRrU634sbTnAYYH7Y4rvD5XTOWja EqbDL/8ogcf+yzmFmpagjs8cnmmt474kBpzlG+GZCwr/TyJJIcqnUeZuIKUTOU0vHJOXCRij DjLGlWwd8Kk+9mZjdaLs+yzUX6gSowGdCDqyY2asy7orWZuABC5g7Wygoi9SVl8gXK9jYE6E 3mW/3OeKsHx2q+3MPxqZBxtDV74sI9hH51m15A3nNcW0GQbgZOc+TwGl33yOJNVw/GbDjJFS DgVztrS+AWg1ldkKyfDwp/6W26d3sp+bsO7JGIX2z44x89PAaaQqrdDmGEmxzjw5RKUevV7k joHnLEr9X0XmOEVuRUk1CTbA7ETAUxwMinllhDO5Ne75vYyBi7nYf2700xwmsqkBbeJr1RHW Xr3TZwlGDd58sR1NF+fmG228Izvf8PcKM4CrhDB2QmVlPBbcdhi85hCzToiI2/2umcpjvI2n QA7l4/vp5CJci1s5P7rWUMeb2ytIZlPpXe1yvwC1seOg9LxQtM7QW5NBcWwC6rvSWN317yvN h7SQmNi7C7DQ/yHW1fYsh8urmqTQc71cSvLdT9JlZM6A0PFbE1H3FJLBnNjwthgR1rsnIu4I CIbrngQ/gKq9UcKk7g1cUG5CiCG+k+pcmtmEcDPakMJsUcSoR+Sa5XW7/ovTXgHpdv4/VDLc irDIF0WaANBEk2cWwK5ZujotYSGqrLIQLL5dqSGYK3S+7YHCbHVldT2g9Egp3HVZ42OJiUwV aRlnBAYDDYiQYKB3GxeLk5f3zTEa8rRzPul0gtwqM33sPHiWQa0oJCKF6MXKtJ3vRa/naaEM eeUwid/MzdRkJ0WlzfOz/AE0VgehjsLFXHlGKkctSPLUKPbm7NGRx8dZSRpMcJU7qU6lgBTM M/fg9nx2/Z2lPkwQ1tCUFXgnImua6loaymlM0jbAU+QKLmcDTjCwsWybK/lDLMM0qNbsBq/v TvdGEjmf3yCmzTvSxGzILRMgSWcb3k88Mm2dhdgD3SmTcqzMEXqdo8qy2dukfto2CCvVyZUK zV3fkJTo6fF6CpZhq46AGld9j9+KvHCnS+F7u7eI5JQsP1xAy0ymfgJhRZyg7ZT8ixAQ+R43 SXIqds76VS7keSUyiZmTxNUq3BKhYOXuG1tPKzY8t9LXnOOr3dvpS2ATg8HoddoEIilo6dL1 t3Gj77+Mh9H+tPQuMYQXo3adJzBP30mPh7kXjXTCUFWKFzjfXGajEtbnvaI83STpZVvsZngl q0FTbpDXUA0HPcXYqyENNkLIZMyUz991LDH0ogH4n2xqBSXT8Jf7Mivvhe6DvDmKTLfhr5BN UNgKVzQIoEaN4m90EtnOAASoQ==
- Ironport-sdr: wXlVSZn299K/YYs//J622CITfiQdWDJF/CJt1zLlfPynv97NUYsw/jb3ANPeVIi/Rt3SZPEiXx rYPUpXkADkdl3l0MR+FGW9U+1dNBqrQV+qqbWZJPhqPIj5TJJ5bI183+IPiqYddr8b1h3Oqipp 6KShIijv/Zxryx94IlmU0Ss2OJeqbNJWdCq5VF2BmWHZ9gX3B4voaOKZ2PVqVJj3fTw8/QowXm f+h01jffJKA9JsUwZCn6hY5PzK/ACYQtumenL4mvBcljwYz3hEYxso/UtQIMlAJSYsN5z+frtq NxnJZc4vxZQtEYMin/hY7Bqn
Hi Qinshi,
I am not sure if it's exactly going to solve your problem, but have a look at the locking and unlocking mechanism in math-comp [1, 2, 3].
Best,
Mukesh
On Wed, 1 Jun 2022 at 22:11, Qinshi Wang <qinshiw AT cs.princeton.edu> wrote:
Hi everyone,Is there any way to make a "Definition" as opaque as a proof ended with "Qed"? My use case is I want to specialize a lemma and defineDefinition foo := lem (* a lot of paramters *).I want to omit its type, which is long. So I cannot start a "Proof." in a normal way.Thanks,Qinshi
- [Coq-Club] Definition as opaque as Qed, Qinshi Wang, 06/01/2022
- Re: [Coq-Club] Definition as opaque as Qed, mukesh tiwari, 06/02/2022
- Re: [Coq-Club] Definition as opaque as Qed, Li-yao Xia, 06/02/2022
- Re: [Coq-Club] Definition as opaque as Qed, Théo Zimmermann, 06/02/2022
- Re: [Coq-Club] Definition as opaque as Qed, Li-yao Xia, 06/02/2022
- Re: [Coq-Club] Definition as opaque as Qed, mukesh tiwari, 06/02/2022
Archive powered by MHonArc 2.6.19+.