Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- type Ordinal (n :: Nat) = Ordinal n
- pattern OLt :: () => forall (n1 :: Nat). (n1 < t) ~ True => Sing n1 -> Ordinal t
- pattern OZ :: forall (n :: Nat). () => (0 < n) ~ True => Ordinal n
- pattern OS :: forall (t :: Nat). KnownNat t => Ordinal t -> Ordinal (Succ t)
- od :: QuasiQuoter
- sNatToOrd' :: (m < n) ~ True => Sing n -> Sing m -> Ordinal n
- sNatToOrd :: (KnownNat n, (m < n) ~ True) => Sing m -> Ordinal n
- ordToNatural :: Ordinal (n :: Nat) -> Natural
- unsafeNaturalToOrd :: SingI (n :: Nat) => Natural -> Ordinal n
- naturalToOrd :: SingI (n :: Nat) => Natural -> Maybe (Ordinal n)
- naturalToOrd' :: Sing (n :: Nat) -> Natural -> Maybe (Ordinal n)
- inclusion :: (n <= m) ~ True => Ordinal n -> Ordinal m
- inclusion' :: (n <= m) ~ True => Sing m -> Ordinal n -> Ordinal m
- (@+) :: (KnownNat n, KnownNat m) => Ordinal n -> Ordinal m -> Ordinal (n + m)
- enumOrdinal :: Sing n -> [Ordinal n]
- absurdOrd :: Ordinal 0 -> a
- vacuousOrd :: Functor f => f (Ordinal 0) -> f a
- ordToInt :: Ordinal n -> Int
- unsafeFromInt :: KnownNat n => Int -> Ordinal n

# Data-types and pattern synonyms

pattern OZ :: forall (n :: Nat). () => (0 < n) ~ True => Ordinal n Source #

Pattern synonym representing the 0-th ordinal.

Since 0.7.0.0

pattern OS :: forall (t :: Nat). KnownNat t => Ordinal t -> Ordinal (Succ t) Source #

Pattern synonym

represents (n+1)-th ordinal.`OS`

n

Since 0.7.0.0

# Quasi Quoter

This section provides QuasiQuoter for ordinals.
Note that,

instance for `Num`

s DOES NOT
checks boundary; with `Ordinal`

, we can use literal with
boundary check.
For example, with `od`

`-XQuasiQuotes`

language extension enabled,
`[`

doesn't typechecks and causes compile-time error,
whilst `od`

| 12 |] :: Ordinal 1`12 :: Ordinal 1`

compiles but raises run-time error.
So, to enforce correctness, we recommend to use these quoters
instead of bare

numerals.`Num`

od :: QuasiQuoter Source #

Quasiquoter for ordinal indexed by GHC's built-n

.`Nat`

Since 0.7.0.0

# Conversion from cardinals to ordinals.

sNatToOrd' :: (m < n) ~ True => Sing n -> Sing m -> Ordinal n Source #

`sNatToOrd'`

`n m`

injects `m`

as `Ordinal n`

.

Since 0.7.0.0

sNatToOrd :: (KnownNat n, (m < n) ~ True) => Sing m -> Ordinal n Source #

`sNatToOrd'`

with `n`

inferred.

Since 0.7.0.0

inclusion :: (n <= m) ~ True => Ordinal n -> Ordinal m Source #

Inclusion function for ordinals.

Since 0.7.0.0

inclusion' :: (n <= m) ~ True => Sing m -> Ordinal n -> Ordinal m Source #

Inclusion function for ordinals with codomain inferred.

Since 0.7.0.0

# Ordinal arithmetics

(@+) :: (KnownNat n, KnownNat m) => Ordinal n -> Ordinal m -> Ordinal (n + m) Source #

Ordinal addition.

Since 0.7.0.0

# Elimination rules for

`Ordinal`

0'

.

`Ordinal`

0'absurdOrd :: Ordinal 0 -> a Source #

Since `Ordinal 0`

is logically not inhabited, we can coerce it to any value.

Since 0.7.0.0

vacuousOrd :: Functor f => f (Ordinal 0) -> f a Source #