A VSCode extension that implements outline view and go to definition for Coq files.
MIT License
A VSCode extension that provides outline view for Coq files.
with
keyword.The extension has not published yet.
To install a beta version, please go to the Github Repo and download latest release.
Then, either press "Cmd-Shift-P" and "Extensions: Install from VSIX", or run code --install-extension coqoutline-0.2.2.vsix
(or whatever version number) from your terminal.
View > Open View
, then search for and select outline
.Go to Definition
or Peek > Peek Definition
in the context menu.
The extension uses regular expressions to analyze Coq documents, thus not all Coq writing styles is accepted. The followings are rules recommended when writing Coq with this extension. Violating them may cause the extension analyze your Coq files in wrong ways.
(* NOT OK *)
Definition (* comment *) name ...
(* OK *)
Definition name ...
(* NOT OK *)
Definition
name ...
(* NOT OK *)
(* anything *) Definition name ...
with
should be treated the same as other key words and follows two rules above.
(* OK *)
Inductive a ...
with b ...
(* NOT OK *)
Inductive a ... with b ...
(* OK *)
Parameters a b c : Type.
Parameters (a : Type) (b c: Type).
(* NOT OK, only a and b will be parsed *)
Parameters a b
c : Type.
(* OK *)
Class A : Type := {
x : Type;
y: Type
}.
(* NOT OK *)
(* should be put in two lines *)
Class B : Type := { i : Type;
(* should be put in two lines *)
j: Type; k: Type
}.
(* OK *)
Inductive A: Type :=
| A | B
| C.
(* NOT OK *)
Inductive A: Type := | A
| B| C.
:=
symbol should be put in the same line as the keyword.
(* OK *)
Module A := B.
(* NOT OK *)
Module A
:= B.
Defined
is treated the same as Qed
, no succeeding ident is allowed.with
keyword (supported)