Data.Type.Ordinal

Data-types

data Ordinal n

class HasOrdinal nat

Conversion from cardinals to ordinals.

sNatToOrd'

sNatToOrd

ordToInt

ordToSing

ordToSing'

data CastedOrdinal n

unsafeFromInt

inclusion

inclusion'

Ordinal arithmetics

(@+)

enumOrdinal

Elimination rules for Ordinal Z.

absurdOrd

vacuousOrd

vacuousOrdM

Quasi Quoter

od