tmEgg
Abstract:
tmEgg is a Coq plugin for the TeXmacs scientific editor. TeXmacs
allows the wysiwyg editing of mathematical documents, much in the
style of LaTeX. Our plugin aims to integrate into a TeXmacs document
mathematics formalised in the Coq proof assistant: formal definitions,
lemmas and proofs. The plugin is still under development. Its main
current hallmark is a document-consistent interaction model, instead
of the calculator-like approach usual for TeXmacs plugins. This means
that the Coq code in the TeXmacs document is interpreted as one
(consistent) Coq file: executing a Coq command in the document means
to execute it in the context (state) of all the Coq commands before
it.