Tej Chajed
Tej Chajed
I want to disable symbol prettification in Haskell strings and comments in particular. It seems like one way to do this is to scope all the prettification rules to not...
There's a performance problem with triggering any prover interaction (most obviously next/previous/go to) from within insert mode. It manifests itself with these operations being much slower in insert mode than...
It's now possible to (unsoundly) disable the positivity check, so the example can use an otherwise-ordinary inductive definition rather than a set of axioms.
Fixes #3069 **What**: Add documentation on getting VS Code support. **Why**: It's not obvious that the styled-components extension will work **How**: **Checklist**: - [x] Documentation - [ ] Tests N/A...
**Description:** In VS Code, you can install the [vscode-styled-components extension](https://marketplace.visualstudio.com/items?itemName=styled-components.vscode-styled-components) to get syntax highlighting for CSS within `` css`...` `` templates. This isn't obviously the right extension to use but...
The README says to use the "from sources" method for "Apple Silicon / M1". This is out of date; there's now a binary dmg release for arm64. Also note that...
An official Coq layer was recently added to develop in pull #6911 - thanks to all who made that possible, especially @bixuanzju! I'm the author of https://github.com/tchajed/spacemacs-coq and use it...
On Coq v8.9 (and also on Coq master, coq/coq@2917fd2cce3a28), the plugin fails to build with the following error: ``` File "src/ast_plugin.ml4", line 439, characters 28-44: Error: Unbound type constructor mutual_inductive...