Safe Haskell | None |
---|
Set-theoretic ordinal arithmetic
- data Ordinal n where
- sNatToOrd' :: (S m :<<= n) ~ True => SNat n -> SNat m -> Ordinal n
- sNatToOrd :: (SingRep n, (S m :<<= n) ~ True) => SNat m -> Ordinal n
- ordToInt :: Ordinal n -> Int
- ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)
- ordToSNat' :: Ordinal n -> CastedOrdinal n
- data CastedOrdinal n where
- CastedOrdinal :: (S m :<<= n) ~ True => SNat m -> CastedOrdinal n
- unsafeFromInt :: forall n. SingRep n => Int -> Ordinal n
- (@+) :: forall n m. (SingRep n, SingRep m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
- enumOrdinal :: SNat n -> [Ordinal n]
Data-types
Set-theoretic (finite) ordinals:
n = {0, 1, ..., n-1}
So, Ordinal n
has exactly n inhabitants. So especially Ordinal Z
is isomorphic to Void
.
Conversion from cardinals to ordinals.
sNatToOrd' :: (S m :<<= n) ~ True => SNat n -> SNat m -> Ordinal nSource
sNatToOrd'
n m
injects m
as Ordinal n
.
sNatToOrd :: (SingRep n, (S m :<<= n) ~ True) => SNat m -> Ordinal nSource
sNatToOrd'
with n
inferred.
ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)Source
Convert Ordinal n
into monomorphic SNat
ordToSNat' :: Ordinal n -> CastedOrdinal nSource
Convert Ordinal n
into SNat m
with the proof of S m :<<= n
.
data CastedOrdinal n whereSource
CastedOrdinal :: (S m :<<= n) ~ True => SNat m -> CastedOrdinal n |
unsafeFromInt :: forall n. SingRep n => Int -> Ordinal nSource
Ordinal arithmetics
(@+) :: forall n m. (SingRep n, SingRep m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)Source
Ordinal addition.
enumOrdinal :: SNat n -> [Ordinal n]Source