/vscoq

Coq Support for Visual Studio Code

Primary LanguageTypeScriptMIT LicenseMIT

A plugin for the Coq Proof Assistant 8.5 and 8.6 in Visual Studio Code.

Features

  • Asynchronous proofs
  • Syntax highlighting
  • Commands: step forward, interpret to point, interrupt computation, queries, set display options, etc.
  • Diff view for proof-view: highlight which terms change between states
  • Smarter editing: does not roll back the state when editing whitespace or comments
  • Works with prettify-symbols-mode
  • Supports _CoqProject
  • The proof-view can be opened in an external web browser
  • LtacProf results treeview

Screenshots

Simple example

Screenshot of Proof Goal

LtacProfiling view:
Simple example