-- The small default Cumulus environment
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Main
import Set.Classes
import Cardinal.Finite
import Nat

-- Main stays small: extensional sets, classes, finite
-- sets, finite cardinality, natural arithmetic, and natural order. In
-- particular, a fresh Workbench buffer can state `Finite(ω)` immediately.
-- Deeper developments use the subject or complete Cumulus entrypoints.