Source files for Lecture Notes, PDF oplss.pdf
To typeset these notes, you will need to have installed LaTeX and the Ott tool. The easiest way to install Ott is through opam.
The Ott tool assists with typesetting mathematical specifications of type systems. All typing rules that appear in the lecture notes are specified within the following source files.
Ott specifications:
- pi.ott - Core system
- bool.ott - Booleans
- sigma.ott - Sigma types
- tyeq.ott - Propositional equality
- epsilon.ott - Irrelevance
- data.ott - Data types
LaTeX source files
- oplss.mng - Main text of the document
- lstpi.sty - Listings specification for typesetting
pi-forallsource code - ottalt.sty - Auxiliary style file for working with Ott produced LaTeX macros
- weirich.bib - BibTeX data
- Makefile - how to put everything together