Safe Haskell | None |
---|
Set-theoretic ordinal arithmetic
- data Ordinal n where
- sNatToOrd' :: (S m :<<= n) ~ True => SNat n -> SNat m -> Ordinal n
- sNatToOrd :: (SingI 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. SingI n => Int -> Ordinal n
- inclusion :: (n :<<= m) ~ True => Ordinal n -> Ordinal m
- inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m
- (@+) :: forall n m. (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
- enumOrdinal :: SNat n -> [Ordinal n]
- od :: QuasiQuoter
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
.
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. SingI n => Int -> Ordinal nSource
inclusion :: (n :<<= m) ~ True => Ordinal n -> Ordinal mSource
Inclusion function for ordinals with codomain inferred.
inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal mSource
Inclusion function for ordinals.
Ordinal arithmetics
(@+) :: forall n m. (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)Source
Ordinal addition.
enumOrdinal :: SNat n -> [Ordinal n]Source
Quasi Quote
Quasiquoter for ordinals