Marco Maggesi

As you say, I think that the most obvious stack of structures is functor > pointed functor > monad. I can do the work (or part of it), if you...

You can use ``` unset_jrh_lexer;; ``` to go back to normal OCaml syntax and ``` set_jrh_lexer;; ``` to reactivate CAML Light / HOL Light syntax.

You need to pick up a good combination of ocaml and camlp5 versions. The one that I'm using right now is the following: ocaml 4.05 camlp5 7.10 there many other...

Hi, I have some instructions for running HOL Light in a Docker container: https://github.com/maggesi/hol-light-docker You may want to start with the usage guide: https://github.com/maggesi/hol-light-docker/blob/master/USAGE.md Actually, I now use a slightly...

Hi @gc00, thank you for your support! The commit I used recently is https://github.com/dmtcp/dmtcp/commit/b0a1ebbadc71e720f4ed476c312cf5b47bab1cef, which comes from the master branch. BTW: you can reproduce my environment by looking at the...

This often comes because you forget to close a backtick (``). It can be solved by closing the backtick, e.g., by sending the sequence `;; Hope it helps.

> How may I correct a single character individuating it with the cursor instead of erasing the whole phrase till the point in question? Short answer: it is not possible....

Use backquote ` not single quote ' (apostrophe) ``` `x+1` ```

> @PetrosPapapa is that the same list for HOL and HOL Light? Yes, and for some other variants of the HOL prover actually.