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

module STLC.README where

-- Syntax and typing rules for STLC
open import STLC.Statics

-- Normalization based on reduction and logical relations
open import STLC.Dynamics

-- NbE based on a presheaf model
open import STLC.NbE