Andrei Burdușa comments

Repositories
Issues
Comments

Results 2 comments of


                                            Andrei Burdușa

agda-mode supresses implicit markdown support from vscode

I'm not using any Markdown extension. This is how VS Code behaves when agda-mode is disabled: ![Screenshot from 2022-08-08 09-54-10](https://user-images.githubusercontent.com/53746396/183357759-2331ec4f-171b-4d32-a99d-fbed27b5872c.png) ![Screenshot from 2022-08-08 09-54-25](https://user-images.githubusercontent.com/53746396/183357765-303d04f5-7022-430b-8d24-235c513631b2.png) It has syntax highlighting and the...

`Set Printing Xyz` options are not honored

I'm working through `Imp.v` from Software Foundations and `Coq> Display Implicit Arguments` seems to have no effect. Interpreting the line ``` Check @ceval_example2. ``` always gives ``` ceval_example2 : empty_st...