Metatheory.lean

-- This module serves as the root of the `Metatheory` library.
-- Import modules here that should be built as part of the library.
import Metatheory.AbstractInterpretation
import Metatheory.AbstractMachines
import Metatheory.AbstractionSafety
import Metatheory.AffineTypes
import Metatheory.AlgebraicEffects
import Metatheory.ANFRegAlloc
import Metatheory.Basic
import Metatheory.Bidirectional
import Metatheory.CL.Confluence
import Metatheory.CL.Parallel
import Metatheory.CL.Reduction
import Metatheory.CL.Syntax
import Metatheory.ContractTypes
import Metatheory.CPS
import Metatheory.CPSTransformation
import Metatheory.CallByPushValue
import Metatheory.CategorySemantics
import Metatheory.Coinduction
import Metatheory.CompilerOptimizations
import Metatheory.ConcurrencyTypes
import Metatheory.Confluence
import Metatheory.DeBruijn
import Metatheory.DependentPattern
import Metatheory.DomainTheory
import Metatheory.EffectHandlers
import Metatheory.EffectSystems
import Metatheory.ElaborationAlgorithm
import Metatheory.Erasure
import Metatheory.Focusing
import Metatheory.GameSemantics
import Metatheory.GradedTypeTheory
import Metatheory.Gradual
import Metatheory.HigherOrderUnification
import Metatheory.HygienicMacros
import Metatheory.InductionRecursion
import Metatheory.InformationFlow
import Metatheory.Intersection
import Metatheory.Lambda.Beta
import Metatheory.Lambda.CBV
import Metatheory.Lambda.Complete
import Metatheory.Lambda.Confluence
import Metatheory.Lambda.Diamond
import Metatheory.Lambda.Eta
import Metatheory.Lambda.Generic
import Metatheory.Lambda.MultiStep
import Metatheory.Lambda.Parallel
import Metatheory.Lambda.Term
import Metatheory.LinearLogic
import Metatheory.LinearTypes
import Metatheory.LogicalRelations
import Metatheory.MacroSystems
import Metatheory.MacroTyping
import Metatheory.MemoryManagement
import Metatheory.MetatheoryGrandTour
import Metatheory.Metrics
import Metatheory.ModalLogic
import Metatheory.ModalTypeTheory
import Metatheory.NormByEval
import Metatheory.Normalization
import Metatheory.OTT
import Metatheory.ObservationalEquality
import Metatheory.ParallelReduction
import Metatheory.Parametricity
import Metatheory.PolymorphismVariants
import Metatheory.ProgramEquivalence
import Metatheory.ProofIrrelevance
import Metatheory.ProofNets
import Metatheory.QuantitativeTypes
import Metatheory.Realizability
import Metatheory.RecursiveTypes
import Metatheory.Refinement
import Metatheory.RefinementTypes
import Metatheory.ResourceLogic
import Metatheory.Rewriting.Basic
import Metatheory.Rewriting.Compat
import Metatheory.Rewriting.DecreasingDiagrams
import Metatheory.Rewriting.DecreasingDiagramsCertificate
import Metatheory.Rewriting.DecreasingDiagramsExternal
import Metatheory.Rewriting.DecreasingDiagramsExternalFamily
import Metatheory.Rewriting.DecreasingDiagramsExternalBenchmarks
import Metatheory.Rewriting.DecreasingDiagramsExample
import Metatheory.Rewriting.DecreasingDiagramsFamily
import Metatheory.Rewriting.Diamond
import Metatheory.Rewriting.HindleyRosen
import Metatheory.Rewriting.Newman
import Metatheory.RowPoly
import Metatheory.STLC.Normalization
import Metatheory.STLC.Terms
import Metatheory.STLC.Types
import Metatheory.STLC.Typing
import Metatheory.STLCext.Complete
import Metatheory.STLCext.Confluence
import Metatheory.STLCext.Normalization
import Metatheory.STLCext.Parallel
import Metatheory.STLCext.Reduction
import Metatheory.STLCext.Terms
import Metatheory.STLCext.Types
import Metatheory.STLCext.Typing
import Metatheory.STLCextBool.CBV
import Metatheory.STLCextBool.Complete
import Metatheory.STLCextBool.Confluence
import Metatheory.STLCextBool.Normalization
import Metatheory.STLCextBool.Parallel
import Metatheory.STLCextBool.Reduction
import Metatheory.STLCextBool.Terms
import Metatheory.STLCextBool.Types
import Metatheory.STLCextBool.Typing
import Metatheory.SecrecyTypes
import Metatheory.SeparationLogic
import Metatheory.Sequent
import Metatheory.SessionProc
import Metatheory.SessionTypes
import Metatheory.SizedTypes
import Metatheory.StackMachineCompilation
import Metatheory.StackMachines
import Metatheory.StringRewriting.Confluence
import Metatheory.StringRewriting.Rules
import Metatheory.StringRewriting.Syntax
import Metatheory.Substructural
import Metatheory.SyntaxTransformers
import Metatheory.SystemF.Complete
import Metatheory.SystemF.ChurchEncodings
import Metatheory.SystemF.Decidability
import Metatheory.SystemF.Confluence
import Metatheory.SystemF.Diamond
import Metatheory.SystemF.Parametricity
import Metatheory.SystemF.Parallel
import Metatheory.SystemF.StrongNormalization
import Metatheory.SystemF.StrongReduction
import Metatheory.SystemF.Standardization
import Metatheory.SystemF.SubjectReduction
import Metatheory.SystemF.Terms
import Metatheory.SystemF.Types
import Metatheory.SystemF.Typing
import Metatheory.TRS.Confluence
import Metatheory.TRS.DiamondComparison
import Metatheory.TRS.FirstOrder.BooleanCaseStudy
import Metatheory.TRS.FirstOrder.CaseStudy
import Metatheory.TRS.FirstOrder.Completion
import Metatheory.TRS.FirstOrder.Confluence
import Metatheory.TRS.FirstOrder.CriticalPairs
import Metatheory.TRS.FirstOrder.DependencyPairs
import Metatheory.TRS.FirstOrder.Examples
import Metatheory.TRS.FirstOrder.GroupTheory
import Metatheory.TRS.FirstOrder.LPO
import Metatheory.TRS.FirstOrder.Ordering
import Metatheory.TRS.FirstOrder.Positions
import Metatheory.TRS.FirstOrder.Rules
import Metatheory.TRS.FirstOrder.Syntax
import Metatheory.TRS.FirstOrder.Unification
import Metatheory.TRS.FirstOrder.UnificationComplete
import Metatheory.TRS.Rules
import Metatheory.TRS.Syntax
import Metatheory.TacticFrameworks
import Metatheory.Termination
import Metatheory.TemporalTypes
import Metatheory.TypeClasses
import Metatheory.TypeInference
import Metatheory.TypeInhabitance
import Metatheory.TypePreservation
import Metatheory.UniversePolymorphism