module index where

-- Typing Context
import context

-- Machine
import config
import machine.eval

-- Simply Typed Lambda Calculus with DeBruijn indecies, types, terms
import stlc.term
import stlc.type

-- Properities of STLC - weakening and exchange
import stlc.properities

-- Monads and implementation
import stlc.monad
import stlc.monad.impl
import stlc.monad.properities

-- Typed Categotrical Cobinators
import stlc.catComb
import stlc.catComb.compile
import stlc.catComb.eval
import stlc.catComb.logicalRelation
import stlc.catComb.betaeta
import stlc.catComb.properities

-- CAM machine instructions
import stlc.inst

-- Values - both combinator values and machine values
import stlc.value
import stlc.value.equality
import stlc.value.properities

-- Step relation
import stlc.step

-- Various proofs of the machine
import stlc.proof.termination
import stlc.proof.wellTyped

-- Untyped Lambda Calculus
import untyped.type
import untyped.context
import untyped.term
import untyped.catComb
import untyped.inst
import untyped.value
import untyped.compile

-- some examples of evaluation of the machine
import stlc.run
import stlc.examples.product
import stlc.examples.coproduct
import stlc.examples.list
import stlc.examples.monad

import untyped.run
import untyped.example