#coq

Rocq Timing

RogerBurtonpatel

Overlay timing information from .v.timing files onto Rocq/Coq source.

LaTeX Command Finder

combinator

Hover over a Unicode character to see the LaTeX command that produces it. Works in any file (Rocq/Coq, Lean, Markdown, plain text, …).

Explore Rocq/Coq proof developments as an interactive dependency graph, with go-to-definition, find-references and live rebuild on save.