Arthur Charguéraud

Hi all. A few answers to the previous messages. - In a default Ubuntu, with the "enable workspaces" option activated, the bindings `CTRL+ALT+Arrows` are reserved for switching workspaces. I think...

Regarding (1) I'd be happy to help out writing a semantics in idiomatic Coq style. Questions, though: should it be Small-step? Big-step? Pretty-big-step? All? Including divergence? I would also be...

Happy to help out by explaining how things work in details to whoever is interested to hack this stuff in CakeML.

``` Fixpoint pat_bindings (p : pat) : list varN := match p with | Pany => [] | Pvar n => n :: [] | Plit l => [] |...

Another occurence is `pmatch`, which takes as last argument an `env`. I think this accumulator could be avoided, simply by making `pmatch_list` concatenate the list of bindings that it gathers,...

Jumping into the discussion with a few comments. - The notion of immutable arrays is useful as a typing information. Sometimes, you'd like the array to be unmodified by a...

I've been very busy lately, I should have time second half of next week to try lsp and this multiple workspace stuff.

My understanding is that coqide is no longer to be developed. I have personally switched to vscode, and I'll try at some point to investigate whether existing extensions can deal...

It would be useful to add in printtyp.mli a number of functions to allow manipulating the type variables obtained from the `qexp_vars` list. In particular, `name_of_type`, `is_non_gen`. I don't recall...

Here are some interesting unit tests, originating from CFML, to check that you capture the polymorphic type variables properly and bind the variables at the right place. ```ocaml let let_poly_p0...