Interactive Mathematical Documents

An application to interactively view Coq contexts and to translate Coq contexts to interactive, human readable OMDoc documents.

Download

	imd.jar	Java class files. This contains the CoqViewer application, the Coq2OMDoc application, the CoqTree datatype, the MathMetaText datatype, and the OMDoc datatype.
	imd-src.tar.gz	Java source files. The sources of the above.
	API Docs	JavaDoc API Documentation of the above.
	leibniz.context	Sample Coq context.

Usage

To start the CoqViewer application:

   java -classpath imd.jar nl.tue.win.martijno.coqviewer.CoqViewer

To transform a context into an OMDoc document you need the OpenMath Java API in your $CLASSPATH.

   java -classpath $CLASSPATH:imd.jar nl.tue.win.martijno.omdoc.Coq2OMDoc foo.context

Links

	Coq Home	The Coq Home Page.
	OMDOC Home	The OMDOC Home Page.
	Up	Up to Martijn's home page.