Discretion.lean

import Discretion.Disc
import Discretion.OrderSupport
import Discretion.Order.Basic
import Discretion.Order.Discrete
import Discretion.Order.Indiscrete
import Discretion.Order.Lattice
import Discretion.FinExcept.Defs
import Discretion.FinExcept.Option
import Discretion.FinExcept.Order
import Discretion.WithDefault
import Discretion.Wk.Nat
import Discretion.Wk.Fin
import Discretion.Wk.List
import Discretion.Wk.Multiset
import Discretion.Wk.Finset
import Discretion.Wk.Set
import Discretion.Wk.Order
import Discretion.Quant.Basic
import Discretion.Quant.Class
import Discretion.Correspondence.Definitions
import Discretion.MorphismProperty.Basic
import Discretion.MorphismProperty.BinaryProducts
import Discretion.MorphismProperty.FiniteProducts
import Discretion.MorphismProperty.CartesianSubcategory
import Discretion.Stream.Action
import Discretion.Submonad.Basic
import Discretion.Trace.Basic
import Discretion.Trace.Elgot
import Discretion.Nonempty.Set
import Discretion.Pom
import Discretion.Premonoidal.Category
import Discretion.Premonoidal.Braided
import Discretion.Premonoidal.Distributive
import Discretion.Premonoidal.CopyDrop
import Discretion.Premonoidal.Property.Basic
import Discretion.Premonoidal.Property.Braided
import Discretion.Premonoidal.Property.WideSubcategory
import Discretion.Premonoidal.Property.Cartesian
import Discretion.Premonoidal.Property.Coherence
import Discretion.Elgot.Monad
import Discretion.Elgot.Category
import Discretion.Elgot.Strong
import Discretion.Resource.Basic
import Discretion.SEC.Intrinsic
import Discretion.SEC.Extrinsic
import Discretion.Monad.Ordered
import Discretion.Monad.Commutative
import Discretion.UB.Basic
import Discretion.UB.Optional
import Discretion.AddMonoidalCategory.Basic
import Discretion.AddMonoidalCategory.ChosenCoproducts