Writing MMT documents with jEdit


In this tutorial, we will write a couple of MMT theories using the MMT language; specifically, we will use jEdit to specify the syntax and proof theory of first-order logic, a simple type theory and views between them using the logical framework LF. This entails creating and building archives and browsing them using the MMT web page.

Preliminaries

You should have MMT and jEdit downloaded and installed according to the instructions here. We will assume, that the directory structure is as recommended there. Furthermore, we will use LF, which is provided by the archive urtheories available on mathhub. So this archive needs to be in the MMT/content directory.


> 1 - Creating Archives