module Substructural.Everything where

-- Public surface for the formalization, including the Section 2 core
-- development and the Section 3 FL specializations.
open import Substructural.Prelude public
open import Substructural.Core.Judgement public
open import Substructural.Core.Rules public
open import Substructural.Core.Derivation public
open import Substructural.Core.Nucleus public
open import Substructural.Core.Extensions public
open import Substructural.Core.Conservation public

-- Section 3 layer (FL and structural extensions).
open import Substructural.FL.Formula public
open import Substructural.FL.Rules public
open import Substructural.FL.Basic public
open import Substructural.FL.Shifts public
open import Substructural.FL.DoubleNegation public
open import Substructural.FL.Glivenko public
open import Substructural.FL.Open public
open import Substructural.FL.Lemma2 public
open import Substructural.FL.Theorem3 public