Grace/Cumulus/Main.g17

Open in Workbench Download source

Imports

Set.Classes · Cardinal.Finite · Nat

Declarations

Source

1-- The small default Cumulus environment2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Main8import Set.Classes9import Cardinal.Finite10import Nat1112-- Main stays small: extensional sets, classes, finite13-- sets, finite cardinality, natural arithmetic, and natural order. In14-- particular, a fresh Workbench buffer can state `Finite(ω)` immediately.15-- Deeper developments use the subject or complete Cumulus entrypoints.16