------------------------------------------------------------------------ -- 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