{-# LANGUAGE UndecidableInstances #-} -- for ErrorPDoc

{- | Unsafe 'Natural' digit renderers.

These are used by "TypeLevelShow.Natural", where modulo arithmetic guarantees
that they are not used unsafely.
-}

module TypeLevelShow.Natural.Digit
  ( ShowNatDigitHexLower, ShowNatDigitHexLowerSym, sShowNatDigitHexLower
  , ShowNatDigitHexUpper, ShowNatDigitHexUpperSym, sShowNatDigitHexUpper
  , ENotDigitOfBase
  ) where

import GHC.TypeNats
import DeFun.Core
import Singleraeh.Equality ( testEqElse )
import TypeLevelShow.Doc
import GHC.TypeLits hiding ( ErrorMessage(..) )

-- | Type-level error message displayed when a digit renderer receives a
--   digit not present in the base it handles.
--
-- Note that we can't show the digit, unless we use 'ShowType'. Which
-- type-level-show is about avoiding. Not really an issue, it should be clear in
-- the type error.
type ENotDigitOfBase base = Text "got non-" :<>: Text base :<>: Text " digit"

-- | Return the associated lower-case 'Char' for a 'Natural' hexadecimal digit.
--
-- Unsafe. Must be called with 0-15.
type family ShowNatDigitHexLower (d :: Natural) :: Char where
    ShowNatDigitHexLower  0 = '0'
    ShowNatDigitHexLower  1 = '1'
    ShowNatDigitHexLower  2 = '2'
    ShowNatDigitHexLower  3 = '3'
    ShowNatDigitHexLower  4 = '4'
    ShowNatDigitHexLower  5 = '5'
    ShowNatDigitHexLower  6 = '6'
    ShowNatDigitHexLower  7 = '7'
    ShowNatDigitHexLower  8 = '8'
    ShowNatDigitHexLower  9 = '9'
    ShowNatDigitHexLower 10 = 'a'
    ShowNatDigitHexLower 11 = 'b'
    ShowNatDigitHexLower 12 = 'c'
    ShowNatDigitHexLower 13 = 'd'
    ShowNatDigitHexLower 14 = 'e'
    ShowNatDigitHexLower 15 = 'f'
    ShowNatDigitHexLower  n = ErrorPDoc (ENotDigitOfBase "hexadecimal")

type ShowNatDigitHexLowerSym :: Natural ~> Char
data ShowNatDigitHexLowerSym d
type instance App ShowNatDigitHexLowerSym d = ShowNatDigitHexLower d

sShowNatDigitHexLower :: Lam SNat SChar ShowNatDigitHexLowerSym
sShowNatDigitHexLower :: Lam SNat SChar ShowNatDigitHexLowerSym
sShowNatDigitHexLower = LamRep SNat SChar ShowNatDigitHexLowerSym
-> Lam SNat SChar ShowNatDigitHexLowerSym
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep SNat SChar ShowNatDigitHexLowerSym
 -> Lam SNat SChar ShowNatDigitHexLowerSym)
-> LamRep SNat SChar ShowNatDigitHexLowerSym
-> Lam SNat SChar ShowNatDigitHexLowerSym
forall a b. (a -> b) -> a -> b
$ \SNat x
sn ->
      SNat x
-> SNat 0
-> ((x ~ 0) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @0) (forall (c :: Char). KnownChar c => SChar c
SChar @'0')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 1
-> ((x ~ 1) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @1) (forall (c :: Char). KnownChar c => SChar c
SChar @'1')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 2
-> ((x ~ 2) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @2) (forall (c :: Char). KnownChar c => SChar c
SChar @'2')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 3
-> ((x ~ 3) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @3) (forall (c :: Char). KnownChar c => SChar c
SChar @'3')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 4
-> ((x ~ 4) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @4) (forall (c :: Char). KnownChar c => SChar c
SChar @'4')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 5
-> ((x ~ 5) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @5) (forall (c :: Char). KnownChar c => SChar c
SChar @'5')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 6
-> ((x ~ 6) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @6) (forall (c :: Char). KnownChar c => SChar c
SChar @'6')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 7
-> ((x ~ 7) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @7) (forall (c :: Char). KnownChar c => SChar c
SChar @'7')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 8
-> ((x ~ 8) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @8) (forall (c :: Char). KnownChar c => SChar c
SChar @'8')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 9
-> ((x ~ 9) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @9) (forall (c :: Char). KnownChar c => SChar c
SChar @'9')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 10
-> ((x ~ 10) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @10) (forall (c :: Char). KnownChar c => SChar c
SChar @'a')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 11
-> ((x ~ 11) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @11) (forall (c :: Char). KnownChar c => SChar c
SChar @'b')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 12
-> ((x ~ 12) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @12) (forall (c :: Char). KnownChar c => SChar c
SChar @'c')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 13
-> ((x ~ 13) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @13) (forall (c :: Char). KnownChar c => SChar c
SChar @'d')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 14
-> ((x ~ 14) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @14) (forall (c :: Char). KnownChar c => SChar c
SChar @'e')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 15
-> ((x ~ 15) => SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @15) (forall (c :: Char). KnownChar c => SChar c
SChar @'f')
    (SChar (ShowNatDigitHexLowerSym @@ x)
 -> SChar (ShowNatDigitHexLowerSym @@ x))
-> SChar (ShowNatDigitHexLowerSym @@ x)
-> SChar (ShowNatDigitHexLowerSym @@ x)
forall a b. (a -> b) -> a -> b
$ forall (doc :: PDoc) a. SingDoc doc => a
errorPDoc @(ENotDigitOfBase "hexadecimal")

-- | Return the associated upper-case 'Char' for a 'Natural' hexadecimal digit.
--
-- Unsafe. Must be called with 0-15.
type family ShowNatDigitHexUpper (d :: Natural) :: Char where
    ShowNatDigitHexUpper  0 = '0'
    ShowNatDigitHexUpper  1 = '1'
    ShowNatDigitHexUpper  2 = '2'
    ShowNatDigitHexUpper  3 = '3'
    ShowNatDigitHexUpper  4 = '4'
    ShowNatDigitHexUpper  5 = '5'
    ShowNatDigitHexUpper  6 = '6'
    ShowNatDigitHexUpper  7 = '7'
    ShowNatDigitHexUpper  8 = '8'
    ShowNatDigitHexUpper  9 = '9'
    ShowNatDigitHexUpper 10 = 'A'
    ShowNatDigitHexUpper 11 = 'B'
    ShowNatDigitHexUpper 12 = 'C'
    ShowNatDigitHexUpper 13 = 'D'
    ShowNatDigitHexUpper 14 = 'E'
    ShowNatDigitHexUpper 15 = 'F'

type ShowNatDigitHexUpperSym :: Natural ~> Char
data ShowNatDigitHexUpperSym d
type instance App ShowNatDigitHexUpperSym d = ShowNatDigitHexUpper d

sShowNatDigitHexUpper :: Lam SNat SChar ShowNatDigitHexUpperSym
sShowNatDigitHexUpper :: Lam SNat SChar ShowNatDigitHexUpperSym
sShowNatDigitHexUpper = LamRep SNat SChar ShowNatDigitHexUpperSym
-> Lam SNat SChar ShowNatDigitHexUpperSym
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep SNat SChar ShowNatDigitHexUpperSym
 -> Lam SNat SChar ShowNatDigitHexUpperSym)
-> LamRep SNat SChar ShowNatDigitHexUpperSym
-> Lam SNat SChar ShowNatDigitHexUpperSym
forall a b. (a -> b) -> a -> b
$ \SNat x
sn ->
      SNat x
-> SNat 0
-> ((x ~ 0) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @0) (forall (c :: Char). KnownChar c => SChar c
SChar @'0')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 1
-> ((x ~ 1) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @1) (forall (c :: Char). KnownChar c => SChar c
SChar @'1')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 2
-> ((x ~ 2) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @2) (forall (c :: Char). KnownChar c => SChar c
SChar @'2')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 3
-> ((x ~ 3) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @3) (forall (c :: Char). KnownChar c => SChar c
SChar @'3')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 4
-> ((x ~ 4) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @4) (forall (c :: Char). KnownChar c => SChar c
SChar @'4')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 5
-> ((x ~ 5) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @5) (forall (c :: Char). KnownChar c => SChar c
SChar @'5')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 6
-> ((x ~ 6) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @6) (forall (c :: Char). KnownChar c => SChar c
SChar @'6')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 7
-> ((x ~ 7) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @7) (forall (c :: Char). KnownChar c => SChar c
SChar @'7')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 8
-> ((x ~ 8) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @8) (forall (c :: Char). KnownChar c => SChar c
SChar @'8')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 9
-> ((x ~ 9) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat  @9) (forall (c :: Char). KnownChar c => SChar c
SChar @'9')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 10
-> ((x ~ 10) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @10) (forall (c :: Char). KnownChar c => SChar c
SChar @'A')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 11
-> ((x ~ 11) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @11) (forall (c :: Char). KnownChar c => SChar c
SChar @'B')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 12
-> ((x ~ 12) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @12) (forall (c :: Char). KnownChar c => SChar c
SChar @'C')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 13
-> ((x ~ 13) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @13) (forall (c :: Char). KnownChar c => SChar c
SChar @'D')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 14
-> ((x ~ 14) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @14) (forall (c :: Char). KnownChar c => SChar c
SChar @'E')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ SNat x
-> SNat 15
-> ((x ~ 15) => SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat x
sn (forall (n :: Nat). KnownNat n => SNat n
SNat @15) (forall (c :: Char). KnownChar c => SChar c
SChar @'F')
    (SChar (ShowNatDigitHexUpperSym @@ x)
 -> SChar (ShowNatDigitHexUpperSym @@ x))
-> SChar (ShowNatDigitHexUpperSym @@ x)
-> SChar (ShowNatDigitHexUpperSym @@ x)
forall a b. (a -> b) -> a -> b
$ forall (doc :: PDoc) a. SingDoc doc => a
errorPDoc @(ENotDigitOfBase "hexadecimal")