Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Julin S <julinshaji01 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] HTML output that remembers proof states step by step
  • Date: Tue, 30 Jul 2024 10:03:09 +0530
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=julinshaji01 AT gmail.com; spf=Pass smtp.mailfrom=julinshaji01 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f51.google.com
  • Ironport-data: A9a23:v+DX2azcQ+/cs0m65VN6t+eswirEfRIJ4+MujC+fZmUNrF6WrkUBz WIXUT/Sa/mMN2L9L9pxaIq/9xsCvpDUzoU1T1Zv+1hgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefSAOCU5NfsYkhZXRVjRDoqlSVtkus4hp8AqdWiCmthg /uryyHkEAHjg28c3l48sfrZ9Esw5qWq4lv0g3RnDRx1lA+G/5UqJMlHTU2BByOQapVZGOe8W 9HCwNmRlo8O10pF5nuNy94XQ2VSKlLgFVDmZkl+B8BOtiN/Shkaic7XAhazhXB/0F1ll/gpo DlEWAfZpQ0BZsUgk8xFO/VU/r0X0QSrN9YrLFDm2fF/wXEqfFP34PBsHkcZELYz68NPBmp83 tVALxI0O0Xra+KemNpXS8Fpj8UnacTpZcYR5ygmwjbeAvIrB5vERs0m5/cChGZ21p0IR6+OI ZdAAdZsREyojxlnOEoTCZQlnO6qhyGmWzJdoVOR46Ew5gA/ySQgi+K3a4aLILRmQ+0PkXykg mHe5V+nC04aMcOEkxOa/yiV07qncSTTA99LTOLpqJaGmma7zWsKTRYSSFGTuui8kkf4WtRFK kVS9DBGkEQp3EmiT924Uh/h5XDZ51gTXN1fF+B84waIokbJ3+qHLnMnSzxTbvMLj+QnYAQt3 W2itovuJwU65dV5Vkmh3ruTqDqzPw0cImkDeTIIQGM5Dz/L8NFbYvXnHoYLLUKlsuAZDw0c1 NxjkcTTr7AajMpO2qfiuF6a2nSjoZ/GSgNz7QLSNo5E0u+bTN/+D2BLwQGEhRqlEGp/Zgfa1 JTjs5bFhN3i9bnXyESwrBwlRdlFHcqtPjzGmkJIFJI87Tmr8HPLVdkPumskdBs5aZ1dKWSBj KrvVeV5tM470JyCPf8fXm5NI517pUQdPY25CKCEM4MUCnSPXFbXrHgxPSZ8IFwBYGB3zPhnZ sbFGSpdJXkdDqtjwXK3QexbuYLHNQhvrV4/savTlkz9uZLHPCD9Ye5cbDOmMLplhIva+1692 4gEZ6O3J+B3CrKWjt//qt5Nczjn7BETWfjLliCgXrTfcls7RD1+UqC5LHFIU9UNopm5X9zgp hmVMnK0AnKj7ZEeAVzSMC4xW6ClRptls3MwMAolOFviiTBpYp+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 EdRJmx3IqSEwBlwjuMaW2muNh1zBiCJ3kn91VFTmHbrdBSqXDaVLUkWG+WEzGYG+U1yIxlZ+ 7C5zj7+cDDIJcve4Ao7aXRHmdfCE+Nj0xLkmd+2OfiFE70RQyvXsoX3aUUm8xLYUN4M3mvZr uxUzcNMQKzcNx9IhZYkCoOfhI8ieDrdKENsGfherb40R0fCczSP2B+LGUC7WuVJA9foqUaYK chfFvhjZiSE9hSlj24kXPYXArpOgvQWysIIeerrKU44orKvlGdVn6yKxBfupl0AYotIqtk8G LPzZjjZM223hFlooUHvgvRAGFKFZYgjWFWh8sGzqP4EBrASgtFKKEsS6Ia5j1+REQlg/i+Xg j/9Wr/r/7Ri5LlozqTREfRlJgSrKNnMevyC3yKtvv9vM97eE8f8mDkEi1vgPjYMZLsYZMtqp O7crP/2w0L3k7IkWE/Jm5S6Nvdo5OfjeMF1I87IPH1hsi/aY/DV4jwH4HGeFZNStcF0v+2Le lOdU9ShUvIwQPJf9W1xRwkFNChFEIXxTKPrhR3lnsS2EhJHjDD2doK2x0HmfURwV3EtKZbhL iTWpvz3xNRTjLoUNS8+H/s8XqNJeg7ya5AHKe/0myKTVFSzo1W4vbDnqxosxBfLBlSAE+f4+ Zj1fQf/RjvjpJD3yMxljKIqsi01FHpdhcwCTnAZ8fNyiBG4CzciBsYZOpMkFJpVs3LT0LfVW TLzV1YhWB7NBWl8TRbB4drdB1bVQqREP9riPTUm8n+Fcyr8VsvKHLJl8Twm+HtsPCfqyOa8M 9wF53nsJV6Lz4p0QfoIrOmO6Qu9Kig2GlpTkaw8ryDzP/raKbAD1XgkEQgUECKaSofCk0LEI WVzTmdBKK1+pYgdDu44E0O52jlA1N8s89nsRSiKydfb/Y6cyYWsDdXhbvrr3ORrgNsifdYzq LCee4dJy2+T030X/6AuvrrFREOy5e2jRqCHEUMoeeHec2xcJIjq0wPuUBfjlP0fxTM=
  • Ironport-hdrordr: A9a23:LAitdKst+yPE2qV6sDfFa9DS7skDT9V00zEX/kB9WHVpm62j5r mTdZEgvyMc5wxhPU3I9erwWpVoBEmslqKdgrNxAV7BZniDhILAFugLhrcKgQeBJ8SUzJ876U 4PSdkZNDQyNzRHZATBjTVQ3+xO/DBPys6Vuds=
  • Ironport-phdr: A9a23:JY20rxwKb2qPGVDXCzJNwFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z xSZuq4m3AGBHd2Cra4e2qyO6+GocFdDyKjCmUhBSqAEbwUCh8QSkl5oK+++Imq/EsTXaTcnF t9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5/I gm6oR/Tu8QYjodvKac8wQbNrndUZuha32xlKUyXkhrm+su84Jtv+DlMtvw88MJNTar1c6MkQ LJCCzgoL34779DxuxnZSguP6HocUmEInRdNHgPI8hL0UIrvvyXjruZy1zWUMsPwTbAvRDSt9 LxrRwPyiCcGLDE27mfagdFtga1BoRKhoxt/w5PIYIyQKfFzcL/Rcc8cSGFcWclfSjFBApikb 4QRE+UBIehWr474p1QUrBu+AxSnCOfgxzJMg3P727Ax3eY8HgHcxAEvENwOv3bUotv7N6kcT P67w7XTwDrZc/9bwy3w5JTUfh0jp/yHQLJ+cdDWyUkqDw7LikiQqYjkPzOTy+8DrnWQ4u1iV eKyj24nqgdxoiOvxsg2iInJh54Zxk3f+CV2xYY6P9y4SEphbdG4F5tQsjiXOo1rScwtX29mo jw1yqEauZGlZigKzowqygPCZvGHfIaG4gzvWPuQLDp2in9ofLKxihW9/0S+yeDyVtW53VZEo yZYkdTBqm4B2wDP58SaSPZx4lus1CqA2Q3V9+pKL0c0la/BJJ4gxL49jpUTsUXfHi/2hUX5l 7WadkQj+uSw5OTnY6nmpp+BN4BvkA3xLqMumsm5DO8lMQYOR3CW9fqg2LDn50H0Q7VHgucon qXEs53WP8QWqrO/DgRIzIsj7wu/Dyy60NsGh3kJMVNFeROZgIXxJ13DJu3zA+2ljFS2ijhrw ujLPr3/DZXJKXjOiLLhcqx8605Y0QY809Jf649NBrEPIP//R1X9tNPfDh8+PAy0x/joBM9h2 YMZXGKDGq6ZMKXMvl+U/u8jPfWAaYsPtDv+K/Up/eDigWI6lFMHfaSlwIMbaHWiEfRnJ0WZb 2DsgtAEEWoSvAo+UejqiFyEUT5IZ3a9RaA85jAnBI67ForDSYWtj6aA3Ce/BJFZemdGClWUH XfubIqLQ+0MZz6KIs99jjwEUqCsR5I52RG0qAD606ZnLvbT+iAAqZ3j08F16/TPmhE26Dx7F N+Q03qNTmFxhmMHXSU63KF5oUxny1eMy7J0g/JCFY8b2/QcWQAjcJXY0uZSCtboWwuHcM3aZ kyhR4CEHDUwSJoKi4sMfkJ8Hc6ihxLCh3OCDLoclrjND5sxpPGPl0PtLtpwni6VnJIqiEMrF 5ceXYXHrqt29gyIQpXMj13cjKGyM6IVwC/K8m6Hi2uIpkBRFgBqAu3eRX5KQEzQoJzi41/aC ae0AOElLw9Az9WCI6lLMoTBglBPRfOlM9PbMCqqg2nlPR+T3fuXaZbyPWAU3SHTEk8BxgIO+ XeALgg3BCb5+krRCTVvERTkZEa/ufJmpiadSUk5hxqPc1Un17ex/UsNgueATvoIwr8ekCIoq jExEVTkmtyLUpyPoA1ueKgaatQ4iLte/UTesQE1fpmpLqQ5w0UbbxwypET2kRN+FoRHl8Eu6 nIs1gt7b6yCghtHcHuD0Jb8N6eySCG69Q2za6PQxlDV0cqHsqYJ5vMirlz/vQavXkM8+nRj2 tNR3jOS/JLPRAYVVJvwVA4w+X0Y7/nYfy084ZjU3H9tafCcvTrL2tZvD+wgi16hc9pZLKKYB VrqCcRJYqrmYOcumlWvclcFJLUIrP9yb57gLaLWnvPyb4MC1Hq8gG9K4Z5wyBeJ/it4EavT2 oodhuqfxk2BXiv9i1Gotob2n5pFbHccBDnaq2CsCYhPa6l1ZYtOB32pJpj9xMh6hpj2W3da9 Qb6L1wD0c6tPxGVahauuG8YnVRSunGhlSaimnZ2jjUoqLGf1S7Pm73Kex8OO2oNT25nxwSJQ 8D8n5URW06maBIsnR2u6BPhxqRVk694KnHaXUZCeyWew3hKaqKrrfLCZsdO7MhtqiBLSKGnZ kjcTLfhohwc2ielHm1ExTl9eSv48pn+mhV7jiqaIhMR5DLbZMVxwwzf7d7dHad50T8PRS0+g j7STlSxJNim+9yImoyL6LjvETL8EMcKIW+2lMuJr2Oj6HdvAAGjkvzW+JWvCgU83SLhlpFrW SjOsBfgc9zu3qW+P/hgexogD1v95sxmX4Bmx9Fo1ddAhD5A38XToCNU9AW7ec9W0q//cncXE DsCwtqOpRPgxFUmNXWRgYTwSnSaxMJlIdi8eGIfnCwnvKUoQO+Z6qJJmSxtrx+2twXUNLJ/g zMcz+Au4Xwb27ghtw8kzyHbCbcXVxo9X2Skh1GT4tayob8CLmSydbm2z0p3n9H5VZmNpwhdX DDyfZJoTkoSpo1vdVnL1nP08ITtftLdOMkSuhOjmBDFl+FJKZg1m6lClW99NGn6p3Fg1/8jg Ekkw8ShpIbeYTYInurxEltCOzbyfc9W5jz9kfMUgJONx472VpR5RmdQAd2xHKruSm5N86ygb VrGESVg+CnHX+CERknGth8g9zWWQvXJfzmWPCVLk4skHUHHYhQZ2EdOBH07hsJrSF7snpCwN hchoGhWvAawqwMQmL0ycUCjFD6O/kHwLW5kLfrXZBtOslMduwGMa5HYtqQrWHgGtpy58F7Uc jzdPlsXSzFPAgveXhjiJuX8vIabtbHJWqzmaaOJOOvry6QWVu/Ul8j3g802onDVbJXJZj47U LU6whYRByknXZmJ3WxeEWpP0HucJ8+D+EXmo3Mx9Jvutq+xHlqovNrqafMaJ9xr/1rebb6rE emWiW45LD9Z0shJ3nrU0P0E20ZUjShydj6rGLBGtCjXTauWlLUFRxgcIzh+MsdF9cdelkFEJ NLbh9Xp17V5ku99ClFLUkbkk92oYspCKn+0NVfODkKGfLqcIjiDz8byaKK6Abpe6Ycc/wW3o iqeGlT/My6rkjDoU1WiM7gJgnzCehNZv465f1BmDm2iBNPqZxunMcNm2D07xbpn4xGCfWUYM DV6bwZMtujKtXIe0qg5QTURqCc8fozm026D4uLVK4gbq65uCyVwzKdB5WgijqBS9GdCTeB0n y3bqphvpUunm6+B0GkCMlIGpzBViYaMpUgnN7/e88wKW2vA/RQW7WySCkxTj9RgA9zr/atXz 5Kc8cC7YCcH6N/S8cYGUoLML9mbNXM6LRfzMDvdDQ9AQDzycG+C3gpSl/ad8nDTpZ8/4MuJ+ tJGWvpQU1o7EekfA0JuEYkZIZt5aTgjlKaSkM8C4XfWRPb5S8BTv5SBXfWXU6yHwNOxgrxNZ h9OyrT9f9x73mzT3kVjbhx3nt2PFReJG99KpSJlY0k/p0AfqBBD
  • Ironport-sdr: 66a86d12_O0+lXY4wtIzhyD7tolcg353WjGg2n1Io+oOWwfZLwkEWy+i x4fSchsht9EDM9p1y+Qsk4PR86a/jqSVGX1VmRg==

Perhaps it's alectryon?

https://alectryon-paper.github.io/snippets/classical.html
https://github.com/cpitclaudel/alectryon

On Tue, Jul 30, 2024 at 8:44 AM Jason Hu <fdhzs2010 AT hotmail.com> wrote:
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.




Archive powered by MHonArc 2.6.19+.

Top of Page