coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Patricia Peratto <psperatto AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Rocq
- Date: Mon, 5 May 2025 10:47:56 -0300
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=psperatto AT gmail.com; spf=Pass smtp.mailfrom=psperatto AT gmail.com; spf=None smtp.helo=postmaster AT mail-pj1-f47.google.com
- Ironport-data: A9a23:IrUbSa9GirhERwkhCJOqDrUDIHqTJUtcMsCJ2f8bNWPcYEJGY0x3m mIeD2uPPPbcMWOheYgnaI6x800CvsfQyIRjQAVrrCtEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPymYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWcpWo4ow/jb8k434ayv4GpwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TE2MlXPH1rYp8hxPdNAll8t sEXMDAEcUXW7w626OrTpuhEg80iKIzzPtpatC0/iz7eCvkiTNbIRKCiCd1whm9hwJATW6yHO YxFNlKDbzyYC/FLEk8MEJ8klfu0gVHwdjRZrBSeoq9fD237lVUsgOWybYOKEjCMbcZ5xm/Gh 0LGxGfCLjI8PcKU5Cqq00v504cjmgugBdtKS+zmnhJwu3WYwXVWAxkLX3OgsPyhgwi/XcheI goa4EITQbMa8UWqSpzlXUT9riLb+BEbXNVUHqsx7wTlJrfoDxixHVQ9fgIcN84fit4MRgQYl WKGh9PgGmk62FGKck61+rCRpDK0HCEaK24eeCMJJTfpBfGz/+nfaTqfHr5e/L6JszHjJd3nL 9m3QMUWgrwSiYsT1fz+8wyYxT2roZfNQ0g+4QC/soOZAuFRNdTNi2+AsAezARN8wGCxEAPpU J8sxZP20Qz2JcvR/BFhuc1UdF1T296LMSfHnXlkFIQ7+jKm9haLJN8Mvmoufxs5Y5hbKVcFh XM/XysBu/e/21P6PcdKj36ZUZVCIVXITIS8D6+NNIImjmZZL1/bong3DaJv44wduBNxyPlga MnznTeEAnEdBqBqhDuwTKF17FPY7nFW+I8nfriil07P+ePGOha9EO5ZWHPQNLxRxP3f+239r Y0PX/ZmPj0FDIUSlAGNrNZLdTjn7BETWfjLliCgXrXbe1E8Rz55Uq65LHFIU9UNopm5X9zgp hmVMnK0AnKh7ZEeAVzSMSwxW6ClRptls3MwMAolOFviiTBpYp+i4O1bP9E7dKUuvr4rh/Nlb eg3S+PZCNR2SxPD52s8a7v5p9dcbxiFv1+FEBekRzkdRKReYTL11OXqRDayyxlWPBGL7ZM/h 5aCyjLkRYEyQlU+LcTON9Oq4VCDnVkcv+NQWUH3DMFZUxju+tIyKgjarPw+E+cTIzrtmxqY0 Ae3B08DhO/v+oUazvjAtZqmnayITdRsPxN9NHbJyJqLLg/mx3qH7a4cdfeXbBbfeXjR+q7/V d5Kzvr5DuILrGxKv6V4Dbxv66A0vPnrmJN30SVmG2ftfX2wK7Y9PESD49ZDhpdNypBdpwGyf ECFofteGLeRPfLaAEwjHxUkYsuDxMMrtGHrt9ptG3rD5Qhz4LajemdRNUPViCVicZ1EALl8y uIl4MMr+wizjyQxCem/jwdWyn+tK0IRWKB2p7AYB47W0jAQ8G9gWqCFKCHK48CoUe5uY20KO T6fgZTQi4tMnnTid2UBLlmT/O5/q6lXhjV04g4jHWmZovvEmf494zNJ+xsVUAl+70tKwsBzC EdRJmx3IqSEwBlwjuMaQGmuNh1zBiTC3kn91VFTmHbrdBSqXDaVLUkWG+WEzGYG+U1yIxlZ+ 7C5zj7+cDDIJcve4Ao7aXRHmdfCE+Nj0xLkmd/9OdaoBLw4XGbVubCvbm82tBfXO8M9q0nZr +1M/uwrS6nEGQMPgq88Ua+26K8xTU2aGWl8Xv1RxqMFMmXCcjWU2zLVCUSQeNtIFsPa432DF M1iCcJeZSuQjB/UgGggOpcNBLtokNoCxtkIIOrrLFFblYqvlGNitZaI+xXugGMufc5Vrv88D YHsbBOHLH2bgCpFum3KrfQcAFGCX/s/WFTe0ty2ocIzLLBSlMF3cEo37Km4gGXNDitj4CCvn V3iY4348rVc7LpCzqrWPIdNPQGWEe/Idf+p9VmzuutebNmUPsbpsRgUm2bdPA9XHOUwXthrp IuJq/ry+l3Ph5ctcmXjg5LaPbJ41caze+t2M8zMM3hRmxWZavLs+xcu/2OZK4RDtdFguu2LY hSeU9TpU/I4QPJfy29xRwkENi0CGoLlaqvEjgGsncSmUxQy/1TOE4K6yCXPc2peSB4tB7T/L Q3R4NOF+dFSqdV3Ni8uXv1JLcdxHw7+ZPEAadb0iDi/C1uoiHOkvp/Jt0IpyRPPO0m+PPfK2 7D3bTmgS03qo4DN9s9TjKJqtB5ODHpdv/g5TnhAx/FI0QKFHEw0BsVDF64ZC6NksD34j7D5Q zDvUFEMKwvAWRZ8TBGtx+i7Aym+ALUCNO6sc3ZttwmRZjytDYyNPKp5+20yqz1qcz/k16e8J ctY5nT0OQOrz4p0QfoIoMa2mvpj2uiQ00dgFZoRSCAuK0127XQ2OH1d8M5lUCXGF4TVlhyOK zRqA29DR06/RAj6FsMIl7u53v0GlGuH8tnqRX7nLBXjV0Gzw+hJyfm5MOb2ulHGRNpfP6YAH BsbWEPUi117GRUvVW8BtNcggKsyAvWOdiR/wGkPWiVK95yNBq8b0w/uUMbBoAzOOOKSLr8Fq gSR3g==
- Ironport-hdrordr: A9a23:fYCWOKkX6zbOGjHiFbhttLjmnmPpDfIB3DAbv31ZSRFFG/Fw9v re5cjzsCWftN9/YgBDpTntAtjifZq+z/5ICOsqTNOftWDd0QPCEGgI1/qE/9SPIVyZysdtkY llN4dzAMDtFlRh5PyKhTWQIpIPxJ2o/smT6ts2DE0AceipUcxdBstCZDpz23cWeDV7
- Ironport-phdr: A9a23:MXxY9xSd0HjAOG+p9hmzlfsiz9psooCVAWYlg6HPa5pwe6iut67vI FbYra00ygOSB8ODs7ke27OM7+jJYi8p39WoiDM4TNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB 89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL58M hm6txndutUZjYd8Kas91wXFr3RVcOlK2G1kIk6ekBn76sqs5pBv9Dhetew8/MBaS6X6eKo4T b1cDDs4Nm0++dPmuxreQwaR/3UQSmoZnAZGDAjD9xH6Q4z+sjDmuepn2SmVJtP5QLYpUjm/9 ahrSRvoiCAaNz4l9Wzcl8J9gL5HrB+nuhdyxZPfboOIO/pkZq7SctMUS2RCUMhMSSJOHpixY JETA+cbJ+tUs5XxqlkIoBCjBQesHuTvyjpQi3Hsx6I6z/4hEQDa0wwhBd0FrW7ao8vvNKgIT eC10K7IxijEYvNOwjf98JbHcgo7rvGQQbJwdtHcyUYqFwzfj1WQrZbpMC+S1uQIqmWW6fdrW u2zhWA9sQ5xviSvydk2ionPno8YyEzJ+ytkzIs3KtC1RkF1bN6gHZdMqy2XNIp7TMM8Tmxop io21rMItYKlcSUKx5oq2QDTZ+GFfoWV/B/uSeecLDFlj3xmYLKynwi+/VSkx+HmVcS50ExGo jRYntTNrHwA2B7e586aQfZj+kehxC2P1xzN5eFePE40lKvaJIA5z7IskJcYrF7NETXsmErsi a+bbkUk9fas6+Tgerjmo4WTN45wig3nKqQumNGzDf02MgUBXWWX4+u81Lrk/U32RLVFkOc6n bXesJDfPcgbp6i5DBFJ0os79RqzEzOr3M4bkHQHNl5JZg+LgonzN1zBIv30FfK/jE6tkDdvy fDGJLrhApDVI3jbi7fhZahy61RGxwov0dBf4IlZCr4EIP3pW0/xsMbUAQM+Mwyx2+rnDs5y2 ZsEWW2TGq+ZLL/SsViQ6+4yO+WMfpMauC7hK/g54P7jlWM2mVgEfaWwwZQXbG24Ee99LkWCY Xvsh88BHn0Qsgo/SuzqklyCXiRJa3a8RaJvrg08XYmhFMLIQp2nqL2HxiayWJNMNU5cDVXZK X70bYSPWv5EUC+IK9N9lXRQTaO5RpUoyQ2pnAD/wrtjaOHT/3tL5trYyNFp6riLxlkJ/jtuA pHFu4nsZ2R9n2dTAiQzwLg6uktljFGKzal/hfVcU91V/fJAFAkgZtbH1+IvLdf0V0rae8uRD k68S4C+Gik8VNst39gmbEN0GtHkhRfGjGKxG7FAr7WQH9Qv977EmX34JsJz0XHDgbE6l1Q8S 9dTMkWpg6d+807YAIua216BmfOMcqIRlDXI6H/FzWeKuxRAVxVsVKzeQX0FTk7frNC8/kGbC rHyVvIoNQxOzcPEIaxPAjHwpXNBQvqreNHXYmbq3ny1GQ7N3bSUKozjZ2Qa2izZTkkCiQEau 3icZ0A4AW+6rmTSASYLdxqnal7w8eR4tHKwT1MlhwCMYUp70rOp+xkTzfWCQvIX17gAtW8vs TJxVFq62tvXDZKHqW8DNO1Eessw+l5byWXxuAl0P5jmJKdnxxYffwlxo0LyxkBvEIwT2cMur X4s0E9zMffCiAIHJ27eh8mufOGIeQyQtFi1ZqXb20/TyoOT86YLs7Ejrkn7+RquDgwk+mlm1 N9c1z2d4I/LBUwcS8GUMA5/+h5kqrXdeiR46ZnT0CgmKbKsvyXLx84uLOQgwxekOdxYNenXc W26W91fHMWoJOEwzhKxdQoJJulO6KkcMMavdv/A06mudrUojHetimJJ55p420SH+n9nS+LG6 J0CxumRwgqNUzqUYE6JisnsgsgEYDgTGjH60i34HMtKYbU0e48XCGCoKsnxx9NkhperVWQKv FKkAloH3oeud3/wJxTlxhVdz00LvXuPli6xzjgymDYs5qaSxy3Bxe3+eQFPYDYaAjk/yw21f 87o0JgTRwCwYhIslQe56EqfpeATv6l5I2TJAA9JcyXwM2B+Q/61v7uGbdRI7cBguiFWXeKgJ FGCH+Sl8l1KjmW5RjUYmG9oElPi8o/0lBF7lm+HeXN6rX6CPNp12Q+a/9vEA/hYwjsBQiB8z zjRHFm1edezrrD239/OtP6zU2W5W9hday7umMmYrzO2/2R2HRqXkPW6m9mhGg8/m3yetZEiR WDToRDwb5O+nbyhKe99d1V0A3fz7sN7Hsd1lY561/RykTAKw56S+3QAi2L6N95WjLn/YHQ6T jkO29fJ4QLh1R4rPjeTyon+THnY3tp5aozwfDYNwixkpZMvau/c/PlekCByuFb9sQ/Bfa03g GIG0fV3oH8C37NS5Ux0n33bWOxNWxEfZ3CklgzUvY7i6v8MPyD2L+D2jA0nzLXDRPmDul0OB ii/I894W3c2toIlaBrNyCGhtN+iIoWBK4JL8EXTyU+IjvAJes1r0KNWw3M2YySl+iR1roxzx R12gcPl4M7ecTgrpOThRUcGfjztO5FKomGr1PkB2JbQh8f1R91gAmlZBcSzC6v5THRK86ygb ljrcnV0q2/HS+CHTEnPtQE/9SKJS9fyaDmWPCVLl4w8AkTNYhUO2kZMG2xr1p8hSlLwnZKnK hwooGtLoAa/80opqKogIRD7Vi23SB6ATDAyRdDfKRNX6loH/ELJKYmF6fo1GShE/5qnpQjLK 2qBZg0OA3tbEkqDT0vuOLWj/7yiu6CRG/a+Iv3SYL6Ptf0WVvGGwoiq25dn+DDEP9uGP31rB fk2kkRZWnUxF8PckjQJAysZ8kCFJ9acvwu58zZro9qX9f3qXEf359LKBecNd9po/B+yjOGIM OvRzCd1JDBE148dkH/FzL9MuTxawypqdjSrDfEBrXuXFPOWyvIRVUdFLX8sZ64qp+om0wJAO NDWkIbw37981bsuDktdEEfmgoevbNALJGe0MBXGAlyKPfKIP26uoYm/bKWiRLlXlOgRuQe3v GPRC1T7My6KiyXufx+qOOBIyiqcOVYN3eP1OgYoEmXlQN/8P1ejN8RriDQt3bAurnbDNGpZK TolNk0R8fuf6iRXhvg5EGtEpCkAT6HMi2OS6O/WLYwTuP1gD3Fvlu5U1389zqNc8CBOQPEdc MT6odtnolXgme6KmGMPuPtmrz9KgMeTvxwnN/mGsJZHXnnA8VQG6mDCU3ziQvNqD9Tuv+Zbz d2dzMrO
- Ironport-sdr: 6818c1e7_Q4TaDKNdluVka4O5Ugbji6zia8JB0ORevAspAbeEa7ampoQ juJSHQamccdc05ZWbw3sFtG1EsnEWxbiKO5/7tQ==
The proofs done in Coq can be used in Rocq ?
Regards.
Patricia
- [Coq-Club] Rocq, Patricia Peratto, 05/05/2025
- Re: [Coq-Club] Rocq, Calvin Beck, 05/05/2025
- Re: [Coq-Club] Rocq, Ralf Jung, 05/09/2025
- Re: [Coq-Club] Rocq, Ralf Jung, 05/09/2025
- Re: [Coq-Club] Rocq, Calvin Beck, 05/05/2025
Archive powered by MHonArc 2.6.19+.