View on GitHub


Type theory with equality reflection


Installation with OPAM

The easiest way to install Andromeda is through the Opam package manager for OCaml. You can install Opam on your system following these instructions. In case your operating system does not provide OCaml version >= 4.02, you can install it with opam switch 4.02.1. Then simply add the Andromeda repo to opam, update and install Andromeda with these commands:

opam repo add andromeda git://
opam update
opam install andromeda

Building Andromeda


To build Andromeda, you need OCaml 4.02 or later (and quite possibly it works with earlier versions too), the menhir parser generator and the sedlex unicode lexer. We recommend using Opam for installation of OCaml, menhir and sedlex.

If you also install the ledit or rlwrap utility, the Andromeda toplevel will use them to give you line editing capabilities.


Checkout the Andromeda repository

git clone

or consider forking it if you indent do contribute to the project.

To build Andromeda type make at the command line. This will create the executable andromeda.native. You can run the tests in the test subfolder with make test.

The file prelude.m31 contains basic definitions and is loaded when Andromeda is started (unless the option --no-prelude is given).