type-natural- Type-level natural and proofs of their properties.

Safe HaskellNone




Set-theoretic ordinal arithmetic



data Ordinal n whereSource

Set-theoretic (finite) ordinals:

 n = {0, 1, ..., n-1}

So, Ordinal n has exactly n inhabitants. So especially Ordinal Z is isomorphic to Void.


OZ :: Ordinal (S n) 
OS :: Ordinal n -> Ordinal (S n) 


SingI Nat n => Bounded (Ordinal (S n)) 
SingI Nat n => Enum (Ordinal n) 
Eq (Ordinal n) 
SingI Nat n => Num (Ordinal n) 
Ord (Ordinal n) 
Read (Ordinal n) => Read (Ordinal (S n)) 
Read (Ordinal Z)

Parsing always fails, because there are no inhabitant.

Show (Ordinal n) 

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 :: (SingI n, (S m :<<= n) ~ True) => SNat m -> Ordinal nSource

sNatToOrd' with n inferred.

ordToInt :: Ordinal n -> IntSource

Convert ordinal into Int.

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.

Quasi Quote

od :: QuasiQuoterSource

Quasiquoter for ordinals