Wolf Honore
Wolf Honore
Attempt at fixing #42. This seems too simple to work, but the tests pass and from playing around with it on the command line everything looks ok to me. Maybe...
This computes the exponential by multiplying the previous result by `base` instead of computing it from scratch with `**` each time, which seems to be about an order of magnitude...
Would it be possible to make the type for `JSON` columns accept `Mapping[str, Any]` instead of (in addition to?) `Dict[str, Any]`? My specific use case is I have a fixed...
```coq Eval cbn in 1 + 1. Definition x := Eval cbn in 1 + 1. Definition y := 2. ``` The second `Eval` is not highlighted, and the second...
Should support interactive ltac debugging provided by [Set Ltac Debug](https://coq.inria.fr/distrib/current/refman/proof-engine/ltac.html#coq:flag.ltac-debug).
Might be interesting to use https://github.com/ejgallego/coq-serapi instead of talking to coqtop directly.
@whonore Is there a way to insert the output of coq inside the current buffer after the line that was just executed? _Originally posted by @ju-sh in https://github.com/whonore/Coqtail/issues/39#issuecomment-809239615_ For example,...
Trying to start Coq on a file under theories/Init fails. ```sh vim $(coqtop -where)/theories/Init/Nat.v +CoqStart # Failed to launch Coq. ``` This seems to be because the `-topfile` option doesn't...
CoqIDE supports asynchronous editing of files where one can work on a later part of a file while the earlier parts are checked in the background. It would be cool...
The syntax files for coq, coq-goals, and coq-infos have a lot of redundancy and some inconsistency. It would be better to define a common files that each can source and...