Skip to Content.
Sympa Menu

coq-club - [Coq-Club] HTML output that remembers proof states step by step

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] HTML output that remembers proof states step by step


Chronological Thread 
  • From: Jason Hu <fdhzs2010 AT hotmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] HTML output that remembers proof states step by step
  • Date: Tue, 30 Jul 2024 03:13:36 +0000
  • Accept-language: en-US, en-CA
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector10001; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=5j2NBXNkPzNy26IQnLCjTkqIL1YvlfxC2wnpNXbYsN0=; b=FuOa1B0xqpGcC1TS8d63uAzkz0/g7t5F5jNLv+P3QzFFgAgWR3tT0a5GbK+9a1UQF4VOBR+H5t47UHUadKYLhDTXuaERwHojNaUVlTmh9ksx0hdQoJnr3Rw3f0eMc/Aj6pP0HXuY6+ZE78HUcXXprgYHZVS1KeMPs926HoL4nh6lbjyYXAiYl0Gm+nYcp3O9+fTEY66sD//S38Rh8ihmVajMz3Y2LUV4nezGfnshotNoTBxO9jNLVIL4EUqJjQVqUNLvTSXUOlurB4523Ku2HghJLZovgXwKI4cmSK8Rlxsh95wWB0N2hpDwEuc6HmfJPW0c5222kgGn5C/8fHXM8w==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector10001; d=microsoft.com; cv=none; b=fb0scyUV/pZtoqfqhRWhtWT3zlhAkCy1u32iicvliMFYut/OVK1LMtshIeqlmY4IxaiVGVZoO7hrNaQaU4vTxEaN1n9dbh2FvODlYZ2TXpQ3VxuJHwZRVnsE9iUw7W0O33AP1/0v8jck3EIOh+jdj/nxGoBDlDrOtgizS3G1+/f33006ercsyOkgBxCywxUecCoUhkjjIsPTFYP+u7Cle1mhDPpto5Y3Tob7tLQB17r+Bd8V8a0RGGq2VeyNjJMBP1NB4A7T8r0SukNaoWl9bpzGzQG53FlDdOfYw9LuI5yHuVBB1uQK5nKiNiy9dXzLu48Q/9jQOGwDRjJ402Z6oQ==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM10-MW2-obe.outbound.protection.outlook.com
  • Ironport-data: A9a23:Ds+4EagHlZFqNEiuVqUoCrWeX161ehsKZh0ujC45NGQN5FlHY01je htvWD3QO6uNYWOhed9wbNzioEMP6J/Vz9JqS1ds/CAyRCJjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqieUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYqdDpFg06/gEk35qiq52lJ5gZWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGIBovA6ED3uBMAk5uy K0nCRUsakmhmLfjqF67YrEEasULCuDOZdtan046iDbTALAhXIzJRLjM6ZlAxjAsi8tSHPHYI c0EdT5oaxeGaBpKUrsVIM5m2rbywCWlNW0FwL6WjfJfD2z7wgBxwqO3aIONUtyNWcBcn0Ler WXDl4j8KkhFa4DEmWHaoxpAgMfkpjnSdogAEYaT3flWpGOxyDQrJgQ/AA7TTf6R0RXkB403x 1Yv0iEptO058FGhZsLsWgWx5n+CpB8VHdRKe9DW8ymIw6vQpgOGXG4NS2cZb9glspVuFWFs0 UKVldT0AzApqKeSVX+W6raTq3W1JDQRKmgBIyQDSGPp/uUPvqkf1QvxYs1HFpW2of3ISA7R5 hGO9Qoh0uB7YdEw6423+lXOgjSJr5fPTxIo6gi/Yo5DxlMpDGJCT9z4gWU3/cp9wJClok5tV UXoduCb5eEKSJSSziqERbxVG7Wq4azdYGCahkNzFZ488Tjr42SkYY1b/DB5IgFuL9oAfjjqJ kTUvGu9BaO/3lP1N8ebgKroUazGKJQM8/y5DZg4ifISOfBMmPevpn0GWKJp9zmFfLIQua8+I 4yHVs2nEGwXD69qpBLvGL1HieRznHthnTqPLXwe8/hB+erPDJJyYedUWGZikshntvvYyOko2 4oBaJfRm00POAEASnaLrN9NcDjm0kTX9bit8JYLKYZv0yJjGWo7DOTWz69pcIt/h8xoehTgr xmAtrtj4AOn3xXvcF3UAlg6Me+Hdcgl8RoTY3d2VX72gCdLXGpaxPxCH3fBVeJ7r7MLID8dZ 6VtRvhs9dwVFmSWpmhBMsCixGGgHTzy7T+z0+OeSGBXV/Zdq8bho7cIpyO2rHVUXBmk/9Azu aOh3Q79SJ8ODVYqRsXPZf7lixv7sXEBkaggFwHFM/tCSnXKqYJKEi3WiuNoAscuLR6Y+CCW+ TzLCjglpM7MgbQPzv/3uY6+ob2UTtRORnhhIzGD7JKdFzXrwW648IoRDMeKZW/8UU33yoWDZ MJU7fb2a8cbrWlOqK55Nahh9oMlxt7Vv7QB5B9VLHbKSFWKC71bPXiN2/dUhJBN3rN0vQiXW FqF39tnZZGlHdzDK0EAAhgHYsCo9+AmqhOL4dsbeEzFtTJKppyZWkBsDjywoS16Lp4uFag6w O0k6fUk2ybmhjUEat+53z1prUKSJXk9UoIihJEQIKnvriEJklhiQ5jtOhXa0aG1SednExcVe 2ePpa/4mb5j6FLIcCMzGVjzzONtv8kyly4Q/mASBWaiu4TjveA27i1z4D5sbwVyzzd76cxRF FVvFXVIIfSpw281qulFB3uhCiNQNi2/o0bR8WYEpEfdbkuvV1HOElEDBPawzBgZ3V5xLjl/1 5OE+VnhSgfvLZ3Q3DNteEtLqM7DbN1W9y/lof3/D+GuRr8Ecxv5iPWMYU4N+kLrLuEviHKap s1s1vd6Mpf/BHUqu6dhV5SQjopIQj/VOmVTHPNrpvsIOUr+eziC/yeEBG7sW8FKJt3MqVSZD e43LO1xdh2O7gS8hRFFOrwpPJlPg+8P2NUZX7HgeEoqkue692JykZTy8iPeujcac+92m5xgF rKLJiOwLGOAoFB1xUrfp9ZgEUila4AmYAbc4riEwN8RHchejNA2IFAA6ZrqjXC7KwA9wgm1u jnEbKroz+BP74Rgso/vM6dbDTWPNtLBe7WUwT+3ruhxQ4vDAeXWuyMRj2vXDQBcEL8SetZwz JCmktr82mHbt7cXDUHdvbS8FJdy2MbjZ9oPb/rLL0RbkxCSB+7qwR8IoF6jJbJzzdhy28iAR imDUvWWS+I7Ydlm6UduW3BsKCpFU6XTRYX8lBy5tMWJW0Q80xSYDdaJ9k3JTGB8dw0PMcbEF j7Lv+2K4/ZGpr9tHz4BPeltWLVjEW/gWIwnVtz/jiaZBW+WmWG/uqPuuB4jyDPTAFyGLZrez bfaYCPhZTKgmq3s5/NIgbxY5xE4Ii50vrgtQxg75dVztQGfMEcHCuY4arAtFZBel33J5qHSP T3iQjMrNnTgYG5ibx753dXEWzWfDMwoPvPSBGQg32GQWheMKLKwOplT3QY+3C4uYRrm9v+tF v8G8H6pPhSR/IBgddxO2tOF29VY1tHo7VNW33vikv7CIQcUWpQL831DIDBjdwL6F+P1qUGaA lRtGE5lRhi3R3ekRIwkMzRQFQoCtTzi8yQwYG3diJzDsoGc16tbxOe5J+j31aYZYd8XIKIVA 0n6XHaJ/3vcz0l7VXHFYD71qfMc5TO38smGwGvLYyQ3xvn1z1t9esQIkGwIUd0o/xNZHxXFj D6w7nMiBUODbkdMxLmRzgZP8JV0Op7JJy+clxbx/FcqjjRgp+U1uTDzpO44FX00g6jko0BRQ TNUZ0GUy7FTnCWxviFw75z3uXTeafz81hD4vuQATpTulx6tTClWE7UJP4TWET5O2CUs+7i4v 5p9HznwFExLk89PM83ZcA8lX4Va
  • Ironport-hdrordr: A9a23:nQFMBKwrXxzrNetZjLWhKrPx8+skLtp133Aq2lEZdPULSKGlfp GV9sjziyWetN9IYgBHpTnyAtj4fZq8z+8A3WB1B9uftWbdyQ+Vxe1ZjLcKoAeQbBEWlNQtsp uIGpIWYLKfMbEQt7eY3ODMKadE/DDxytHLuQ6x9RdQZDAvT5slwxZyCw6dHEEzbhJBH4AFGJ 2V4dcCjya8eFwMB/7LT0UtbqzmnZnmhZjmaRkJC1oM8w+Vlw6l77b8DlyxwgoeaTVS2r0vmF K12zARp5/T+c1Sh3fnpiTuBqZt6ZfcI+h4dYOxY/0uW3jRYl7BXvUuZ1TNhkF1nAjl0idTrD CFmWZaAy000QKmQom4zCGdoTUI/Qxem0MK82Xo8kfLsIj8XnY3GsBBjYVWfl/Q7Fchpsh11O ZO03iCv5RaABvclGCljuK4Ii1Chw6xuz4vgOQTh3tQXc8Xb6JQt5UW+AdQHI0bFCz35Yg7GK 1lDd3a5vxRbVSGBkqpzFWG67SXLwkO9zu9Mzk/U5auokdrdVhCvjUlLOx2pAZ9yK4A
  • Ironport-phdr: A9a23:RllTLBJ4DGXMh8mZBtmcuNFuWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCEvbMy1xSXDM2bs6sC17CH9fi4GCQp2tWojjMrSN92a1c9k8IYnggtUoauKHbQC7rUVRE8B 9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9I Ri4sQndrMsbjIVtJqswzhbCv39Ed/hLyW9yKl+fgRLx6t2s8JJ/9ihbpu4s+dNHXajmcKs0S qBVAi4hP24p+sPgqAPNTRGI5nsSU2UWlgRHDg3Y5xzkXZn/rzX3uPNl1CaVIcP5Q7Y0WS+/7 6hwUx/nlD0HNz8i/27JjMF7kb9Wrwigpxx7xI7UfZ2VOf9jda7TYd8WWWxMVdtKWidfHo2zc ZcAD+sZPeZZsYb9oUcOrQCjDgWoHe/j1yNEimPz0aA81OsvDBzG3Bc4H90QrHvUsNv7NKAXU e+vzanIyyjIY/dZ1Dr57YTFdA0qr/ORUrJqacffyVchGR7ZjlueqoLqIzya2/8XvGSH8+ZtT /6jh3I6pwx3vzOhxt0sio7Mho8Nzl7L7z55wIEzJdalSkB7fMOvHZxety6HN4t3Q9giT390t Con1rELop67fC8WyJQi3RHfaviHf5KU7RLkUeacODF1j29qd7yjnRi961SgyvHiWcmu1lZHt i5In8XPu30Q2BHf98eJRPVh8kqu2DuC1QDe5/1ZLUwpmqTWKposzLEtmpYOsUnOGi37lUT1g aKZd0gq9PWk5vjhb777qJGcMIp0hRv/MqQogsG/DuU4MhQOX2iG4uuwzrzj/Ur/Tb5XjfM2i rHUvZ/GKcgBoqO1HRVZ34k95xqlDDqr0MwUkWcGIV5Zdh+KipXlN03VL/35CPqyg0mgnCtuy vzbMbDuHpDAI33BnbrnYL1w9UpcyBcozdBD+Z1UEKwPIPPyW0DvrNHUEhk0OBGuzen9EtVyz IYeVHqPAqCHNKPStkeF6PozLueLeYMZpC/xJf8l6PLwlHM5nkQScrez0ZsQdXC4Au9pI0KEY Xrqn9gNC38KvhA5TOz2llKNTSJTZ3e1X6I6/D07D5+mDZvHRoCqh7yB3z23EYFRZmBDElyME HHoeJuYW/oUZy+ePtVtnzgaWbS7RIItywuiuQz6xrZ/K+rb4CwYtZbt1Nhv4O3TkAk/9TJpA MSd0mCNVH94kn8VSzMqx61/oUt9ykuG0adigvxYEcZf6O9OUgc/LZLcyfd1BMjoWg3dZteJV EqmQtK+DD0sVt4x2cMBY15hG9W+iRDOxzalA7gMl7CSGJM09r/c0GPqKsZmy3fG0bEhgEM8T stOM22mnK9/+BLJC47HiUXK35qtII8bxWbm8HqJhT6Fu1gdWwptW43EW2oebw3Yt4KqyFnFS uqMAK8gNENh1IbWJKdKeMaz1QwebPfkJNHXYmb3kGC1U0XbjoiQZZbnLj1OlB7WD1IJxkVOp B5uVCA7Dyal+SfFCSB2UEjoaAXq+PV/r3WySgk1yRuLZgtvzen94QYb0NqbTf5bxbcYoGE5s TwhElq9zcmMU4PYjwpmYKBVYNd761BChirCrwIoBpW7NOh5g0IGNQF+vkfgzRJyX4tMkdox9 itzlCJyLr6d2VJFMTif2MO4IaXZf1H75wvncKvKwhfe3dKRr78I8+g9ok7/sRuBMGMHqi0i9 uYPlnyW69PNERYYVo/3XgAv7R9mqrrGYy47oYTJyXlrNqryuTjHsz4wLM0izBvoP9JWMafeU RT3D9VfHc+lbuojh1muaBsAeuFU7q89ec28JbOA3+awMeBskSjD7ywP6Z1h0k+K6yt3S/LZl 5cDzfaC2wKbVjD6xF6/u8HzkIpAaHkcBG26gSTjAYdQYOV1c+NpQS+gL82l3Y8m3sbFW3lE8 VeiAxUN38roMRueYlrh3BFBgFwNqC/vki+5wjpo1jAx+/bHmn2Uhbi4MkpaaQspDCF4gFzhI Ja5lYUfVUmsNU0ykQe9oFz9zO5drbh+KG/aRQFJeTL3JidsSPjV1PLKbshR5ZcvqSgSXv67Z AXQRLL9sQBAi3q7N2tZ2DUydjXssZL81U8f6irVPDNooXzVdNsljxnT5M7HH6YIhhIGQzV9g DjTQFO7OpP6mLfc34eGuee4WWW7U5RVeiS+1oKMuhyw4mhyCAG+lfS+8jH+OTAzyjSzl9xjV CGS6Q35fpGuzaOxd+RuYkhvAlb4rct8AIB31IUq1tkc3n0Th5Pd+nRi8y+7P9lby7mkNCNVb T4M39vc4Qyj00pmZn6E3IP2UHyBz9ApO4H8MzlQhnh7v50CAbzc9LFemCppvle0yGCZKeNwm DsQ07pm6XIXhf0IpBt4yyycBr4IGkwLdSfolhmO85W/tPALPCD+K/7sjgwuwIPEbvnKuAxXV Xfnd413GCZx6p86K1fQyDjp7YqiftDMbNUVvxnSkhHajuETJohi85hCzSdhJ2/5umUojuAhi hk7l5+2vJqccT00pIq5BQJdPzzxIcgU/3u+6MQW1tbTxI2pEph7T38FUJv6VqjwSWo6tfP7M g+PFHs3rXLRSt+9VUePrUxhqXzICZWiMXqacWIYwdtVTx6YPEVDgQoQUWZyjtsjGwut3sCkb FZh62Vb+AvjshUVgLENVVG3QiLFqQyvcDtxVJWPME8c8FRZ/0mMec2GsrAuRWcBpsbn9ErVb TXELwVQUTNQAhDCWw+lZv/2ooCflorQTuumc6mSOfPf86oGEa/PnMzn05M6rW/UaoPTYT84V 7tjnRAYFXFhR5aAw2lJF3NRznqdKZbc/kzZmGU/r9jjoq2zBESzus3QVv0Kdo8zsxGu3fXab 7LW2Hk/dG0ei8tLnyOAyaBBjgQb03g8LmD0Q7pc7XafHuWMyso1R1Yac30hbsIQtvBlh1AfN 5KD0YGnkeIpxv8tVQUfXAS4yJjwPJ4EfznmZgOfXB7ZZvPbfVipi4n2ef3uE7QI1bcN7kTit 2rDSB3oZmzbxWuuCknnMPkS3nuSZEUM4djkIBgxUTOxQoq+Mk/pd4ItxXg/xbl+7p/THVYVK iM0M0ZEr7nKqDhdnu06AWtKqHxsMeiDnS+dqejeMJcf9/VxUGx4kOdT4XJyzLUwjmkMXPtuh C7btcJjuXmAu8zWkn9Cb0ALrTxGwoWWoU9lJKPVsIFaXmrJ9w4M6mPWDAkWo9xiCZvkvKU1q JCHmK/oKThE+s7Z5oNAX46FcoTbajxxbFLgA3bMAREATCK3OG2XnEFbnPyItzWUopU8tpnwi c8OR7tcBzlXXrsRDkVoGsBHIY8iAmtiwOTd0JROtSftyXuZDN9XtZ3GSP+IVPDmKTLDyKJBe wNN27Tza4IaKoz83UVmLFh8hoXDXUTKDrUv6mVsaBE5pEJV/T1wVGo2jgjrZgO/+yVLTKacn hkqjwJ/ZaIm8zKmsDJVbhLa4TA9lkU8g4CvmTeKbDv4N7u9R6lwIg+t7w0UDcm+RAx4Kwqvg UZjKTHIAapLiKdtfnxqjwmavoZTHflbTutPZxpalpT1L704lF9brCug30pO4+DIXIBjmAUde pmpt3tc2ghnYY19NenKKaFO1FQVmrOWs3riyLUq2AFHbRVokivaaGsStUcPLLVjOye44rkm9 1mZgzUaMGkUC6h2+rQ7rAVlfbzHln+o0qYfeBzpcbXHcOXB/TCHzJDtIBt411tUxRQfu+Eui YF7NRLTDhxnzaPNRU1RaYyedkcNKZIVrSebfD7Q47/EmcsnZtzkRO60Fbfc5uFI0ifGVE4oB 9petM1ZR8v1iRiKI5u/d+xXjkl8rAXzegffBawQKkvSyWUJ/5nkns8vhdEPdHZAWAAfeW22/ uiF/AZy2ajaBY5kbCtCBdkPbipuCp/9xncRvmweXmO+irtLkVHbvTGg/n+CAmGkN4gxI6rOL VZlDNX8kd3e246frAePt7DhfST9P9kkvcLT4+QHoZrBE+lTUbR2r0bbnc9fWmCuVGnMV9WyI sqpA2HJRdzzFnOzU1j5gDUwHZ+Z1DmFLq+UhAjpQcBft4zJhVge
  • Ironport-sdr: 66a85a67_Rh+XkRLU61GZ3QKBb1R5XCHo4UgcUN+9Hlj4XqCZIrpoEtl 8QJK6D0Bt6ctmdAwx4Nq4b+63iWET2bmdEEQpxg==
  • Msip_labels:

Hi all,

I vaguely remember someone's Coq HTML artifact that remembers all proof states so that I was able to inspect proof step by step in the browser. I don't seem to find anything on Google. Do I remember it incorrectly? Any more verbose output than what coqdoc already provides is appreciated.

Thanks,
Jason Hu
https://hustmphrrr.github.io/



Archive powered by MHonArc 2.6.19+.

Top of Page