View on GitHub

Andromeda 1

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.07, you can install it with opam switch 4.08.1. Then simply add the Andromeda repo to opam, update and install Andromeda with these commands:

git clone
cd andromeda
git checkout andromeda-1.0
opam update
opam pin add andromeda .    # for installation (confirm twice with "y")

# to upgrade
cd andromeda
git pull
opam upgrade

# to uninstall
opam uninstall andromeda-1
opam pin remove andromeda-1

Building Andromeda


To build Andromeda, you need OCaml 4.07 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 and dependencies.

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
git checkout andromeda-1.0

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).