Arthur Charguéraud
Arthur Charguéraud
Hi, I am the author of the `re` tool: https://github.com/charguer/re which also aims at saving time with `cd` commands. I think the tool has features that would nicely completes those...
Here are my suggestions for keybindings. Based on years of practice by myself and students, moreover designed to take best advantage of the new "vos" feature. If you don't buy...
Ideally, auxiliary functions used in the semantics should have the simplest possible presentation, and not use accumulators. E.g. `pat_bindings` currently has type `pat -> list varN -> list varN` but...
Loops can be encoded using tail-ref functions. Yet, they are incredibly useful in the surface language. Especially for describing algorithms. Many graph algorithms take the form `while not (queue.is_empty()) do...
A famous example of a very useful or-pattern is the following balance function from Okasaki's presentation of red-black trees: ``` let balance = function | (Black, Node (Red, Node (Red,...
When clauses are very useful for writing concise ML code. Yet, it is very hard to give them a semantics. On the one hand, it is useful to allow the...
VsCoq currently supports only a global setting of the `coqProjetRoot` variable. When working on a project with several folders, each featuring its own Coq root,* one needs to use a...
Consider the file LibList.v from the TLC library (part of the Coq CI). This compiles in batch mode (coqc) in 3.7 seconds (with a single core). VSCoq1 processes it in...