Safe Haskell | None |
---|---|
Language | Haskell2010 |
- type Ordinal n = Ordinal n
- pattern OLt :: forall t. () => forall n1. (~) Bool ((:<) Nat n1 t) True => Sing Nat n1 -> Ordinal Nat t
- pattern OZ :: forall n. () => (~) Bool ((:<) Nat Z n) True => Ordinal Nat n
- pattern OS :: forall t. SingI Nat t => Ordinal Nat t -> Ordinal Nat (Succ Nat t)
- od :: QuasiQuoter
- sNatToOrd' :: (m :< n) ~ True => Sing n -> Sing m -> Ordinal n
- sNatToOrd :: (SingI n, (m :< n) ~ True) => Sing m -> Ordinal n
- ordToInt :: Ordinal n -> Integer
- unsafeFromInt :: SingI n => MonomorphicRep (Sing :: Nat -> Type) -> Ordinal n
- inclusion :: (n :<= m) ~ True => Ordinal n -> Ordinal m
- inclusion' :: (n :<= m) ~ True => Sing m -> Ordinal n -> Ordinal m
- (@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
- enumOrdinal :: Sing n -> [Ordinal n]
- absurdOrd :: Ordinal Z -> a
- vacuousOrd :: Functor f => f (Ordinal Z) -> f a
Data-types and pattern synonyms
pattern OLt :: forall t. () => forall n1. (~) Bool ((:<) Nat n1 t) True => Sing Nat n1 -> Ordinal Nat t Source #
pattern OZ :: forall n. () => (~) Bool ((:<) Nat Z n) True => Ordinal Nat n Source #
Pattern synonym representing the 0-th ordinal.
Since 0.7.0.0
pattern OS :: forall t. SingI Nat t => Ordinal Nat t -> Ordinal Nat (Succ Nat 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 Peano numeral
.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 :: (SingI n, (m :< n) ~ True) => Sing m -> Ordinal n Source #
sNatToOrd'
with n
inferred.
Since 0.7.0.0
unsafeFromInt :: SingI n => MonomorphicRep (Sing :: Nat -> Type) -> Ordinal n Source #
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
(@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m) Source #
Ordinal addition.
Since 0.7.0.0
Elimination rules for Ordinal
Z
.
Ordinal
Z