{-# OPTIONS --safe #-}   -- This ensures everything imported in this module is safe.
{-# OPTIONS --with-K #-} -- This is for the pattern calculus only.
module Everything where

-- Well-staged lists and trees. Used to define the typing contexts.
import Data.StagedList

import Data.StagedTree

-- λ◯▷
import CtxTyp.Context

import CtxTyp.Term

import CtxTyp.Term.Properties

import CtxTyp.Depth

import CtxTyp.Substitution

import CtxTyp.Substitution.Properties

import CtxTyp.Reduction

import CtxTyp.Examples

import CtxTyp.Denotational

import CtxTyp.Denotational.Adequacy

-- Translation from λ◯▷ to λ◯
import Splice.Context

import Splice.Term

import Splice.Translate

-- λ◯▷pat
import Pat.Context

import Pat.Context.Equality

import Pat.Term

import Pat.Term.Equality

import Pat.Matching

import Pat.Depth

import Pat.Substitution

import Pat.Rewriting

import Pat.Reduction

import Pat.Examples

import Pat.Denotational