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 112 :: 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 #