module A201802.Everything where


--------------------------------------------------------------------------------

import A201801.Prelude

import A201801.Category

import A201801.Fin
import A201801.FinLemmas

import A201801.Vec
import A201801.VecLemmas
import A201801.AllVec


--------------------------------------------------------------------------------

import A201802.LR0
import A201802.LR0Lemmas
import A201802.LR1
import A201802.LR2
import A201802.LR3


--------------------------------------------------------------------------------

import A201801.List
import A201801.ListLemmas

import A201801.AllList

import A201801.FullIPLPropositions


--------------------------------------------------------------------------------

import A201802.WIP.Bool -- TODO: reuse
import A201802.WIP.Name -- TODO: reuse
import A201802.WIP.ListRemovals -- TODO: reuse
import A201802.WIP.CoquandList -- TODO: reuse

import A201802.WIP.CoquandStyle -- TODO: unfinished
import A201802.WIP.LocallyNameless -- TODO: unfinished
import A201802.WIP.NotLocallyNameless -- TODO: unfinished

import A201802.WIP.CurryHoward -- TODO: broken

import A201802.WIP.LR1a

import A201802.WIP.LR2 -- TODO: unfinished
import A201802.WIP.LR2-NoECs
import A201802.WIP.LR2a
import A201802.WIP.LR2b
import A201802.WIP.LR2c
import A201802.WIP.LR2d
import A201802.WIP.LR2e -- TODO: unfinished

import A201802.WIP.LR3 -- TODO: which LR2?
import A201802.WIP.LR3a -- TODO: unfinished; which LR2?
import A201802.WIP.LR3b -- TODO: missing id-cons-WKS-SUBS; which LR2?
import A201802.WIP.LR3-Mutual -- TODO: unfinished; which LR2?
import A201802.WIP.LR3NonMutual -- TODO: which LR2?

import A201802.WIP.LR4 -- TODO: unfinished; which LR2?

import A201802.WIP.LR-scratch


--------------------------------------------------------------------------------