PeaCoq
PeaCoq copied to clipboard
Ptival
PeaCoq is a pretty Coq, isn't it?
Bumps [d3-selection](https://github.com/d3/d3-selection) from 1.4.2 to 3.0.0. Release notes Sourced from d3-selection's releases. v3.0.0 Adopt type: module. #281 Allow selection.merge to take a transition. #257 Allow selection.join to take transitions. #286...
![dependabot-preview[bot] avatar](https://avatars.githubusercontent.com/in/2141?v=4 "dependabot-preview[bot] avatar"){kind=avatar}
Bumps [d3-path](https://github.com/d3/d3-path) from 1.0.9 to 3.0.1. Release notes Sourced from d3-path's releases. v3.0.1 Update dependencies. Make build reproducible. v3.0.0 Adopt type: module. This package now requires Node.js 12 or higher....
This is just a suggestion, but IMHO it would make sense to implement a small Coq program that given an OCaml type [for example, `constr_expr` , the Coq's AST] would...
Hi Valentin, When I saw this today, I was quite happy: ``` PEACOQ: This seems to be NixOS, use nix-shell before calling setup.sh or set NIXSHELL ``` But to get...
Would be pretty slick :wink: I'm thinking something like https://try.jupyter.org/
[This blog post](http://goto.ucsd.edu/~vrobert/coq-en-stock/blog/2015/06/03/introducing-peacoq/) discusses the tool in detail with screenshots. Some of that information should probably be included on the website and in the README! In fact, the website should...
Right now the server runs without a warning!
This one may be asking a bit much:  The goal is False, Knight B is a hypothesis, and there's a nice, juicy contradiction bi-implied by it. This case...
Hi, this is an idea I've had to use peacoq's existing work to generate annotated coq files to get things like http://homes.cs.washington.edu/~jrw12/dep-destruct.html where you can mouse over the proof in...
I can send you the code to repro the issue if you need it. `htop` shows minimal memory usage (out of 16GB) and 1 of 8 cores being used 100%...
