Data.Type.Ordinal

Data-types

data Ordinal n

Conversion from cardinals to ordinals.

sNatToOrd'

sNatToOrd

ordToInt

ordToSNat

ordToSNat'

data CastedOrdinal n

unsafeFromInt

inclusion

inclusion'

Ordinal arithmetics

(@+)

enumOrdinal

Elimination rules for Ordinal Z.

absurdOrd

vacuousOrd

vacuousOrdM

Quasi Quoter

od