Hi! This is an ongoing shortcoming of jsCoq; the API exists but it is quite unstable and not documented. Here is a small snippet that showcases loading jsCoq and programmatically invoking some proof manipulation, that I created for a similar request in the past.
it assumes jsCoq installed via NPM (
npm install jscoq from the same directory that contains
playful.html; then serve the directory over http).
Hi Shachar, thanks for this, that is very helpful! I'll give it a peruse.
Hi @Archibald Neil MacDonald , I'm busy today, I will get back to you with more detail soon, but someone did already implement a blocky frontend for jsCoq
let me contact them and see if the code is available already
That is absolutely adorable!!
Last updated: Jan 30 2023 at 18:04 UTC