Skip to content
GitLab

Add VS code to the editor.md docs

Merged Jules Jacobs requested to merge jules/iris:vscode-editor-docs into master

Added VS code to editor.md:

  • Which extension to use for Coq.
  • How to get a good unicode font that supports all the Iris symbols.
  • Which extension to use for unicode input.
  • A configuration file to configure unicode input for Iris (e.g. \later). Commands copied from those for CoqIDE..