Data.Type.Ordinal

Data-types

data Ordinal n

class HasOrdinal nat

Quasi Quoter

mkOrdinalQQ

odPN

odLit

Conversion from cardinals to ordinals.

sNatToOrd'

sNatToOrd

ordToInt

ordToSing

unsafeFromInt

inclusion

inclusion'

Ordinal arithmetics

(@+)

enumOrdinal

Elimination rules for Ordinal Z.

absurdOrd

vacuousOrd