Grace/Cumulus/Ordinal.g17

Open in Workbench Download source

Imports

Set.Ordinal.Arithmetic · Set.Ordinal.OrderType · Set.Ordinal.Monotone · Set.Ordinal.ArithmeticLaws · Set.Ordinal.Omega

Declarations

Source

1-- Ordinal numbers: their order, arithmetic, and the cumulative hierarchy2-- 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.Ordinal8import Set.Ordinal.Arithmetic9import Set.Ordinal.OrderType10import Set.Ordinal.Monotone11import Set.Ordinal.ArithmeticLaws12import Set.Ordinal.Omega13