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

-- Simplified core calculus, without contextual types
import Core.Context

import Core.Term

import Core.Depth

import Core.Substitution

import Core.Reduction

import Core.Examples

import Core.Denotational

-- Core calculus with contextual arrow type
import CtxArr2.Context

import CtxArr2.Term

import CtxArr2.Depth

import CtxArr2.Substitution

import CtxArr2.Reduction

import CtxArr2.Examples

import CtxArr2.Denotational

-- Core calculus with contextual arrow type and its dual
import CtxTyp.Context

import CtxTyp.Term

import CtxTyp.Depth

import CtxTyp.Substitution

import CtxTyp.Reduction

import CtxTyp.Examples

import CtxTyp.Denotational

-- Translation from CtxTyp to λ◯

import Splice.Context

import Splice.Term

import Splice.Translate

-- Pattern calculus
import Pat.Context

import Pat.Context.Equality

import Pat.Term

import Pat.Term.Equality

import Pat.Matching

import Pat.Rewriting

import Pat.Depth

import Pat.Substitution

import Pat.Reduction

import Pat.Examples

import Pat.Denotational