module A201606.Everything where


--------------------------------------------------------------------------------

import A201606.Common.UntypedContext
import A201606.Common.Context
import A201606.Common.Delay
import A201606.Common.StrongBisimilarity
import A201606.Common.OrderPreservingEmbedding

import A201606.STLC.Syntax
import A201606.STLC.HereditarySubstitution
import A201606.STLC.CoinductiveNormalisationByEvaluation
import A201606.STLC.Examples

import A201606.PfenningDaviesS4.Syntax
import A201606.PfenningDaviesS4.HereditarySubstitution -- TODO: unfinished
import A201606.PfenningDaviesS4.HereditarySubstitution2 -- TODO: unfinished
import A201606.PfenningDaviesS4.HereditarySubstitution3 -- TODO: unfinished
import A201606.PfenningDaviesS4.HereditarySubstitution4 -- TODO: unfinished
import A201606.PfenningDaviesS4.CoinductiveNormalisationByEvaluation
import A201606.PfenningDaviesS4.Examples

import A201606.BonelliSterenLP.Syntax -- TODO: unfinished


--------------------------------------------------------------------------------