------------------------------------------------------------------------
-- Normalisation for the simply typed λ-calculus
------------------------------------------------------------------------

module README where

------------------------------------------------------------------------
-- Using de Bruijn indices

-- The type system.

import SimplyTyped.TypeSystem

-- Applicative structures.

import SimplyTyped.ApplicativeStructure

-- Environments.

import SimplyTyped.Environment

-- Evaluating terms.

import SimplyTyped.Evaluation

-- Context extensions.

import SimplyTyped.ContextExtension

-- Substitutions.

import SimplyTyped.Substitution

-- Normal forms.

import SimplyTyped.NormalForm

-- Values.

import SimplyTyped.Value

-- Normalisation.

import SimplyTyped.Normalisation

-- Semantics (not used for anything).

import SimplyTyped.Semantics
import SimplyTyped.Semantics.Lemmas

------------------------------------------------------------------------
-- Using PHOAS

-- The following modules mirror most of the development above, but use
-- HOAS (more specifically, Adam Chlipala's PHOAS) instead of
-- de Bruijn indices.

import HOAS.SimplyTyped.TypeSystem
import HOAS.SimplyTyped.Evaluation
import HOAS.SimplyTyped.NormalForm
import HOAS.SimplyTyped.Value
import HOAS.SimplyTyped.Normalisation

-- A condensed version of the HOAS.SimplyTyped modules above (no
-- comments, but no imports and less than one page long).

import HOAS.SimplyTyped