Right now this is a laboratory to experiment in implementing dependent types.

git clone https://github.com/bitonic/tog
cd tog
make

If you want to install the binary

make install

To type check files

tog [FILE]

There are various options, most notably -i to get a GHCi-like prompt, and -d to get debug output. -d '' will give you a complete dump of all the debug output, that is to say a lot of stuff.

tog --help gives the full options.

See examples/ for some example files, it's basically a simple Agda.

To run the (sadly quite limited) tests, run

make test

Top-level module interface:

import           Conf
import           PrettyPrint
import           Syntax
import qualified Syntax.Raw                       as SR
import qualified Syntax.Abstract                  as SA
import           Term
import           TypeCheck3