{-# OPTIONS --without-K --safe #-}

module T.README where

-- static semantics
import T.Statics

-- nbe operations for β equivalence
import T.Semantics
-- (partial) completeness for nbe
import T.Strict


-- nbe operations for βη equivalence
import T.TypedSem
-- completeness for nbe
import T.PER
-- soundness for nbe
import T.Soundness