Valentin Robert
Valentin Robert
While color is great when you want it, it can be annoying when you don't. https://no-color.org/ This manifesto suggests supporting a `NO_COLOR` environment variable that disables all color codes when...
I don't think this is coq-serapi's fault per se, but I find this behavior a little annoying to deal with: ``` (0 (Control (StmAdd () "Require Import List."))) (Answer 0...
Hello! This is a very selfish request, but I'd love it if there was a way to have: ``` A__subA_B__subB ``` render with the `sub` things being subbed, and the...
I don't know how uniform people's environments are, but for all my projects I have something along the lines of: ``` `- root `- _CoqProject `- Makefile `- Makefile.coq `-...
Not sure you can do much about it, but I can't seem to install doom-emacs via home-manager on NixOS. I keep getting: ``` error: opening directory '/nix/store/qzcy2dq1fba86d34k0d6apdirkxkxnp7-source': Too many open...
Some type classes provide default implementations as functions (since default members are not supported yet). However, to use those, one needs eta-expand them, or the compiler will yell that the...
When Coq starts up, typing `->` inserts `->` and displays `→`. But from the moment a single `proof-unicode-toggle` command is issued, typing `->` will always insert `→` (and of course,...
It seems that the `:=` from the tactic `have := ...` confuses the indentation mechanism. After it, lines are indented as far as after the `:=` symbol. Not sure how...
The following two commands: ``` Goal 2 + 2 = 5. {| I can write whatever I want here... |}. ``` are being processed correctly by my version of PG+coq....
I'm not sure whether this is related to: https://github.com/ProofGeneral/PG/issues/427 I have a generated file that contains extremely long one-line definitions (think > 10,000 characters). When these lines are being displayed,...