{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
module Data.Type.Ordinal
(
Ordinal (..),
pattern OZ,
pattern OS,
od,
sNatToOrd',
sNatToOrd,
ordToNatural,
unsafeNaturalToOrd',
unsafeNaturalToOrd,
reallyUnsafeNaturalToOrd,
naturalToOrd,
naturalToOrd',
ordToSNat,
inclusion,
inclusion',
(@+),
enumOrdinal,
absurdOrd,
vacuousOrd,
)
where
import Data.Maybe (fromMaybe)
import Data.Ord (comparing)
import Data.Proxy (Proxy (Proxy))
import Data.Type.Equality
import Data.Type.Natural
import Data.Type.Natural.Core (SNat (..))
import Data.Typeable (Typeable)
import Language.Haskell.TH.Quote
import Numeric.Natural
import Unsafe.Coerce
data Ordinal (n :: Nat) where
OLt :: (n < m) => SNat (n :: Nat) -> Ordinal m
{-# COMPLETE OLt #-}
fromOLt ::
forall n m.
((Succ n < Succ m), KnownNat m) =>
SNat (n :: Nat) ->
Ordinal m
fromOLt :: SNat n -> Ordinal m
fromOLt SNat n
n = SNat n -> Ordinal m
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat n
n
pattern OZ :: forall (n :: Nat). (0 < n) => Ordinal n
pattern $bOZ :: Ordinal n
$mOZ :: forall r (n :: Nat).
(0 < n) =>
Ordinal n -> (Void# -> r) -> (Void# -> r) -> r
OZ <- OLt Zero where OZ = SNat 0 -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat 0
sZero
pattern OS :: forall (t :: Nat). (KnownNat t) => Ordinal t -> Ordinal (Succ t)
pattern $bOS :: Ordinal t -> Ordinal (Succ t)
$mOS :: forall r (t :: Nat).
KnownNat t =>
Ordinal (Succ t) -> (Ordinal t -> r) -> (Void# -> r) -> r
OS n <-
OLt (Succ (fromOLt -> n))
where
OS Ordinal t
o = Ordinal t -> Ordinal (Succ t)
forall (n :: Nat). KnownNat n => Ordinal n -> Ordinal (Succ n)
succOrd Ordinal t
o
deriving instance Typeable Ordinal
instance (KnownNat n) => Num (Ordinal n) where
Ordinal n
_ + :: Ordinal n -> Ordinal n -> Ordinal n
+ Ordinal n
_ = [Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"Finite ordinal is not closed under addition."
Ordinal n
_ - :: Ordinal n -> Ordinal n -> Ordinal n
- Ordinal n
_ = [Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"Ordinal subtraction is not defined"
negate :: Ordinal n -> Ordinal n
negate Ordinal n
_ = [Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"There are no negative oridnals!"
Ordinal n
_ * :: Ordinal n -> Ordinal n -> Ordinal n
* Ordinal n
_ = [Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"Finite ordinal is not closed under multiplication"
abs :: Ordinal n -> Ordinal n
abs = Ordinal n -> Ordinal n
forall a. a -> a
id
signum :: Ordinal n -> Ordinal n
signum = [Char] -> Ordinal n -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"What does Ordinal sign mean?"
fromInteger :: Integer -> Ordinal n
fromInteger = Natural -> Ordinal n
forall (n :: Nat). KnownNat n => Natural -> Ordinal n
unsafeFromNatural' (Natural -> Ordinal n)
-> (Integer -> Natural) -> Integer -> Ordinal n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral
unsafeFromNatural' :: forall n. KnownNat n => Natural -> Ordinal n
unsafeFromNatural' :: Natural -> Ordinal n
unsafeFromNatural' Natural
k = Natural
-> (forall (n :: Nat). KnownNat n => SNat n -> Ordinal n)
-> Ordinal n
forall r.
Natural -> (forall (n :: Nat). KnownNat n => SNat n -> r) -> r
withSNat Natural
k ((forall (n :: Nat). KnownNat n => SNat n -> Ordinal n)
-> Ordinal n)
-> (forall (n :: Nat). KnownNat n => SNat n -> Ordinal n)
-> Ordinal n
forall a b. (a -> b) -> a -> b
$ \SNat n
sk ->
case SNat n
sk SNat n -> SNat n -> SBool (n <? n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <? m)
%<? KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat @n of
SBool (n <? n)
STrue -> SNat n -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat n
sk
SBool (n <? n)
SFalse -> [Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error ([Char] -> Ordinal n) -> [Char] -> Ordinal n
forall a b. (a -> b) -> a -> b
$ [Char]
"Index out of bounds: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Natural, Natural) -> [Char]
forall a. Show a => a -> [Char]
show (Natural
k, Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal @n Proxy n
forall k (t :: k). Proxy t
Proxy)
instance
(KnownNat n) =>
Show (Ordinal (n :: Nat))
where
showsPrec :: Int -> Ordinal n -> [Char] -> [Char]
showsPrec Int
d Ordinal n
o = Char -> [Char] -> [Char]
showChar Char
'#' ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
showParen Bool
True (Int -> Natural -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
d (Ordinal n -> Natural
forall (n :: Nat). Ordinal n -> Natural
ordToNatural Ordinal n
o) ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char] -> [Char]
showString [Char]
" / " ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
d (SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural (SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n)))
instance Eq (Ordinal (n :: Nat)) where
Ordinal n
o == :: Ordinal n -> Ordinal n -> Bool
== Ordinal n
o' = Ordinal n -> Natural
forall (n :: Nat). Ordinal n -> Natural
ordToNatural Ordinal n
o Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Ordinal n -> Natural
forall (n :: Nat). Ordinal n -> Natural
ordToNatural Ordinal n
o'
instance Ord (Ordinal (n :: Nat)) where
compare :: Ordinal n -> Ordinal n -> Ordering
compare = (Ordinal n -> Natural) -> Ordinal n -> Ordinal n -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Ordinal n -> Natural
forall (n :: Nat). Ordinal n -> Natural
ordToNatural
instance
(KnownNat n) =>
Enum (Ordinal (n :: Nat))
where
fromEnum :: Ordinal n -> Int
fromEnum = Natural -> Int
forall a. Enum a => a -> Int
fromEnum (Natural -> Int) -> (Ordinal n -> Natural) -> Ordinal n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ordinal n -> Natural
forall (n :: Nat). Ordinal n -> Natural
ordToNatural
toEnum :: Int -> Ordinal n
toEnum = Natural -> Ordinal n
forall (n :: Nat). KnownNat n => Natural -> Ordinal n
unsafeFromNatural' (Natural -> Ordinal n) -> (Int -> Natural) -> Int -> Ordinal n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral
enumFrom :: Ordinal n -> [Ordinal n]
enumFrom = Ordinal n -> [Ordinal n]
forall (n :: Nat). KnownNat n => Ordinal n -> [Ordinal n]
enumFromOrd
enumFromTo :: Ordinal n -> Ordinal n -> [Ordinal n]
enumFromTo = Ordinal n -> Ordinal n -> [Ordinal n]
forall (n :: Nat).
KnownNat n =>
Ordinal n -> Ordinal n -> [Ordinal n]
enumFromToOrd
enumFromToOrd ::
forall (n :: Nat).
(KnownNat n) =>
Ordinal n ->
Ordinal n ->
[Ordinal n]
enumFromToOrd :: Ordinal n -> Ordinal n -> [Ordinal n]
enumFromToOrd Ordinal n
ok Ordinal n
ol =
(Natural -> Ordinal n) -> [Natural] -> [Ordinal n]
forall a b. (a -> b) -> [a] -> [b]
map
(SNat n -> Natural -> Ordinal n
forall pxy (n :: Nat). KnownNat n => pxy -> Natural -> Ordinal n
reallyUnsafeNaturalToOrd (SNat n -> Natural -> Ordinal n) -> SNat n -> Natural -> Ordinal n
forall a b. (a -> b) -> a -> b
$ KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat @n)
[Ordinal n -> Natural
forall (n :: Nat). Ordinal n -> Natural
ordToNatural Ordinal n
ok .. Ordinal n -> Natural
forall (n :: Nat). Ordinal n -> Natural
ordToNatural Ordinal n
ol]
enumFromOrd ::
forall (n :: Nat).
(KnownNat n) =>
Ordinal n ->
[Ordinal n]
enumFromOrd :: Ordinal n -> [Ordinal n]
enumFromOrd Ordinal n
ord =
(Natural -> Ordinal n) -> [Natural] -> [Ordinal n]
forall a b. (a -> b) -> [a] -> [b]
map
(Proxy Any -> Natural -> Ordinal n
forall pxy (n :: Nat). KnownNat n => pxy -> Natural -> Ordinal n
reallyUnsafeNaturalToOrd Proxy Any
forall k (t :: k). Proxy t
Proxy)
[Ordinal n -> Natural
forall (n :: Nat). Ordinal n -> Natural
ordToNatural Ordinal n
ord .. Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal @n Proxy n
forall k (t :: k). Proxy t
Proxy Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1]
enumOrdinal :: SNat (n :: Nat) -> [Ordinal n]
enumOrdinal :: SNat n -> [Ordinal n]
enumOrdinal SNat n
sn = SNat n -> (KnownNat n => [Ordinal n]) -> [Ordinal n]
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn ((KnownNat n => [Ordinal n]) -> [Ordinal n])
-> (KnownNat n => [Ordinal n]) -> [Ordinal n]
forall a b. (a -> b) -> a -> b
$ (Natural -> Ordinal n) -> [Natural] -> [Ordinal n]
forall a b. (a -> b) -> [a] -> [b]
map (Proxy Any -> Natural -> Ordinal n
forall pxy (n :: Nat). KnownNat n => pxy -> Natural -> Ordinal n
reallyUnsafeNaturalToOrd Proxy Any
forall k (t :: k). Proxy t
Proxy) [Natural
0 .. SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural SNat n
sn Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1]
succOrd :: forall (n :: Nat). (KnownNat n) => Ordinal n -> Ordinal (Succ n)
succOrd :: Ordinal n -> Ordinal (Succ n)
succOrd (OLt SNat n
n) =
SNat (n + 1) -> Ordinal (Succ n)
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt (SNat n -> SNat (n + 1)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc SNat n
n)
{-# INLINE succOrd #-}
instance (KnownNat n, 0 < n) => Bounded (Ordinal n) where
minBound :: Ordinal n
minBound = SNat 0 -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat 0
sZero
maxBound :: Ordinal n
maxBound = SNat (n - 1) -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt (SNat (n - 1) -> Ordinal n) -> SNat (n - 1) -> Ordinal n
forall a b. (a -> b) -> a -> b
$ KnownNat (n - 1) => SNat (n - 1)
forall (n :: Nat). KnownNat n => SNat n
sNat @(n - 1)
unsafeNaturalToOrd ::
forall (n :: Nat).
(KnownNat n) =>
Natural ->
Ordinal n
unsafeNaturalToOrd :: Natural -> Ordinal n
unsafeNaturalToOrd Natural
k =
Ordinal n -> Maybe (Ordinal n) -> Ordinal n
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> Ordinal n
forall a. HasCallStack => [Char] -> a
error [Char]
"unsafeNaturalToOrd Out of bound") (Maybe (Ordinal n) -> Ordinal n) -> Maybe (Ordinal n) -> Ordinal n
forall a b. (a -> b) -> a -> b
$
Natural -> Maybe (Ordinal n)
forall (n :: Nat). KnownNat n => Natural -> Maybe (Ordinal n)
naturalToOrd Natural
k
unsafeNaturalToOrd' ::
forall proxy (n :: Nat).
(KnownNat n) =>
proxy n ->
Natural ->
Ordinal n
unsafeNaturalToOrd' :: proxy n -> Natural -> Ordinal n
unsafeNaturalToOrd' proxy n
_ = Natural -> Ordinal n
forall (n :: Nat). KnownNat n => Natural -> Ordinal n
unsafeNaturalToOrd
{-# WARNING reallyUnsafeNaturalToOrd "This function may violate type safety. Use with care!" #-}
reallyUnsafeNaturalToOrd ::
forall pxy (n :: Nat).
(KnownNat n) =>
pxy ->
Natural ->
Ordinal n
reallyUnsafeNaturalToOrd :: pxy -> Natural -> Ordinal n
reallyUnsafeNaturalToOrd pxy
_ Natural
k =
Natural
-> (forall (n :: Nat). KnownNat n => SNat n -> Ordinal n)
-> Ordinal n
forall r.
Natural -> (forall (n :: Nat). KnownNat n => SNat n -> r) -> r
withSNat Natural
k ((forall (n :: Nat). KnownNat n => SNat n -> Ordinal n)
-> Ordinal n)
-> (forall (n :: Nat). KnownNat n => SNat n -> Ordinal n)
-> Ordinal n
forall a b. (a -> b) -> a -> b
$ \(SNat n
sk :: SNat k) ->
(((n + 1) <=? n) :~: 'True)
-> ((((n + 1) <=? n) ~ 'True) => Ordinal n) -> Ordinal n
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((() :~: ()) -> ((n + 1) <=? n) :~: 'True
forall a b. a -> b
unsafeCoerce (() :~: ()
forall k (a :: k). a :~: a
Refl :: () :~: ()) :: (k <? n) :~: 'True) (((((n + 1) <=? n) ~ 'True) => Ordinal n) -> Ordinal n)
-> ((((n + 1) <=? n) ~ 'True) => Ordinal n) -> Ordinal n
forall a b. (a -> b) -> a -> b
$
SNat n -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat n
sk
sNatToOrd' :: (m < n) => SNat (n :: Nat) -> SNat m -> Ordinal n
sNatToOrd' :: SNat n -> SNat m -> Ordinal n
sNatToOrd' SNat n
_ = SNat m -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt
{-# INLINE sNatToOrd' #-}
sNatToOrd :: (KnownNat n, m < n) => SNat m -> Ordinal n
sNatToOrd :: SNat m -> Ordinal n
sNatToOrd = SNat n -> SNat m -> Ordinal n
forall (m :: Nat) (n :: Nat).
(m < n) =>
SNat n -> SNat m -> Ordinal n
sNatToOrd' SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat
naturalToOrd ::
forall n.
(KnownNat n) =>
Natural ->
Maybe (Ordinal (n :: Nat))
naturalToOrd :: Natural -> Maybe (Ordinal n)
naturalToOrd = SNat n -> Natural -> Maybe (Ordinal n)
forall (n :: Nat). SNat n -> Natural -> Maybe (Ordinal n)
naturalToOrd' (SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n)
naturalToOrd' ::
SNat (n :: Nat) ->
Natural ->
Maybe (Ordinal n)
naturalToOrd' :: SNat n -> Natural -> Maybe (Ordinal n)
naturalToOrd' SNat n
sn Natural
k = Natural
-> (forall (n :: Nat). KnownNat n => SNat n -> Maybe (Ordinal n))
-> Maybe (Ordinal n)
forall r.
Natural -> (forall (n :: Nat). KnownNat n => SNat n -> r) -> r
withSNat Natural
k ((forall (n :: Nat). KnownNat n => SNat n -> Maybe (Ordinal n))
-> Maybe (Ordinal n))
-> (forall (n :: Nat). KnownNat n => SNat n -> Maybe (Ordinal n))
-> Maybe (Ordinal n)
forall a b. (a -> b) -> a -> b
$ \(SNat n
sk :: SNat pk) ->
case SNat n
sk SNat n -> SNat n -> SBool (n <? n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <? m)
%<? SNat n
sn of
SBool (n <? n)
STrue -> Ordinal n -> Maybe (Ordinal n)
forall a. a -> Maybe a
Just (SNat n -> Ordinal n
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat n
sk)
SBool (n <? n)
_ -> Maybe (Ordinal n)
forall a. Maybe a
Nothing
ordToSNat :: Ordinal (n :: Nat) -> SomeSNat
ordToSNat :: Ordinal n -> SomeSNat
ordToSNat (OLt SNat n
n) = SNat n -> (KnownNat n => SomeSNat) -> SomeSNat
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => SomeSNat) -> SomeSNat)
-> (KnownNat n => SomeSNat) -> SomeSNat
forall a b. (a -> b) -> a -> b
$ SNat n -> SomeSNat
forall (n :: Nat). KnownNat n => SNat n -> SomeSNat
SomeSNat SNat n
n
{-# INLINE ordToSNat #-}
ordToNatural ::
Ordinal (n :: Nat) ->
Natural
ordToNatural :: Ordinal n -> Natural
ordToNatural (OLt SNat n
n) = SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural SNat n
n
inclusion' :: (n <= m) => SNat m -> Ordinal n -> Ordinal m
inclusion' :: SNat m -> Ordinal n -> Ordinal m
inclusion' SNat m
_ = Ordinal n -> Ordinal m
forall a b. a -> b
unsafeCoerce
{-# INLINE inclusion' #-}
inclusion :: (n <= m) => Ordinal n -> Ordinal m
inclusion :: Ordinal n -> Ordinal m
inclusion (OLt SNat n
a) = SNat n -> Ordinal m
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt SNat n
a
{-# INLINE inclusion #-}
(@+) ::
forall (n :: Nat) m.
(KnownNat n, KnownNat m) =>
Ordinal n ->
Ordinal m ->
Ordinal (n + m)
OLt SNat n
k @+ :: Ordinal n -> Ordinal m -> Ordinal (n + m)
@+ OLt SNat n
l = SNat (n + n) -> Ordinal (n + m)
forall (n :: Nat) (m :: Nat). (n < m) => SNat n -> Ordinal m
OLt (SNat (n + n) -> Ordinal (n + m))
-> SNat (n + n) -> Ordinal (n + m)
forall a b. (a -> b) -> a -> b
$ SNat n
k SNat n -> SNat n -> SNat (n + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n
l
absurdOrd :: Ordinal 0 -> a
absurdOrd :: Ordinal 0 -> a
absurdOrd (OLt SNat n
_) = case (0 :~: 1
forall k (a :: k). a :~: a
Refl :: 0 :~: 1) of
vacuousOrd :: (Functor f) => f (Ordinal 0) -> f a
vacuousOrd :: f (Ordinal 0) -> f a
vacuousOrd = (Ordinal 0 -> a) -> f (Ordinal 0) -> f a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Ordinal 0 -> a
forall a. Ordinal 0 -> a
absurdOrd
od :: QuasiQuoter
od :: QuasiQuoter
od =
QuasiQuoter :: ([Char] -> Q Exp)
-> ([Char] -> Q Pat)
-> ([Char] -> Q Type)
-> ([Char] -> Q [Dec])
-> QuasiQuoter
QuasiQuoter
{ quoteExp :: [Char] -> Q Exp
quoteExp = \[Char]
s -> [|OLt $(quoteExp snat s)|]
, quoteType :: [Char] -> Q Type
quoteType = [Char] -> [Char] -> Q Type
forall a. HasCallStack => [Char] -> a
error [Char]
"No type quoter for Ordinals"
, quotePat :: [Char] -> Q Pat
quotePat = \[Char]
s -> [p|OLt ((%~ $(quoteExp snat s)) -> Equal)|]
, quoteDec :: [Char] -> Q [Dec]
quoteDec = [Char] -> [Char] -> Q [Dec]
forall a. HasCallStack => [Char] -> a
error [Char]
"No declaration quoter for Ordinals"
}