-- | Character predicates.

-- TODO for singling, I could cheat by inspecting the char value. should be
-- faster and better. but would need a bit more checking so cba for now.

module Symparsec.Parser.While.Predicates where

import DeFun.Core
import GHC.TypeLits
import Singleraeh.Bool
import Singleraeh.Equality ( testEqElse )
import Unsafe.Coerce ( unsafeCoerce )

class SingChPred chPred where
    singChPred :: Lam SChar SBool chPred

-- | @A-Za-z@
type IsAlpha :: Char -> Bool
type family IsAlpha ch where
    IsAlpha 'a' = True
    IsAlpha 'A' = True
    IsAlpha 'b' = True
    IsAlpha 'B' = True
    IsAlpha 'c' = True
    IsAlpha 'C' = True
    IsAlpha 'd' = True
    IsAlpha 'D' = True
    IsAlpha 'e' = True
    IsAlpha 'E' = True
    IsAlpha 'f' = True
    IsAlpha 'F' = True
    IsAlpha 'g' = True
    IsAlpha 'G' = True
    IsAlpha 'h' = True
    IsAlpha 'H' = True
    IsAlpha 'i' = True
    IsAlpha 'I' = True
    IsAlpha 'j' = True
    IsAlpha 'J' = True
    IsAlpha 'k' = True
    IsAlpha 'K' = True
    IsAlpha 'l' = True
    IsAlpha 'L' = True
    IsAlpha 'm' = True
    IsAlpha 'M' = True
    IsAlpha 'n' = True
    IsAlpha 'N' = True
    IsAlpha 'o' = True
    IsAlpha 'O' = True
    IsAlpha 'p' = True
    IsAlpha 'P' = True
    IsAlpha 'q' = True
    IsAlpha 'Q' = True
    IsAlpha 'r' = True
    IsAlpha 'R' = True
    IsAlpha 's' = True
    IsAlpha 'S' = True
    IsAlpha 't' = True
    IsAlpha 'T' = True
    IsAlpha 'u' = True
    IsAlpha 'U' = True
    IsAlpha 'v' = True
    IsAlpha 'V' = True
    IsAlpha 'w' = True
    IsAlpha 'W' = True
    IsAlpha 'x' = True
    IsAlpha 'X' = True
    IsAlpha 'y' = True
    IsAlpha 'Y' = True
    IsAlpha 'z' = True
    IsAlpha 'Z' = True
    IsAlpha _   = False

type IsAlphaSym :: Char ~> Bool
data IsAlphaSym ch
type instance App IsAlphaSym ch = IsAlpha ch

sIsAlphaSym :: Lam SChar SBool IsAlphaSym
sIsAlphaSym :: Lam SChar SBool IsAlphaSym
sIsAlphaSym = LamRep SChar SBool IsAlphaSym -> Lam SChar SBool IsAlphaSym
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep SChar SBool IsAlphaSym -> Lam SChar SBool IsAlphaSym)
-> LamRep SChar SBool IsAlphaSym -> Lam SChar SBool IsAlphaSym
forall a b. (a -> b) -> a -> b
$ \SChar x
ch ->
      SChar x
-> SChar 'a'
-> ((x ~ 'a') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'a') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'a') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'A'
-> ((x ~ 'A') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'A') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'A') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'b'
-> ((x ~ 'b') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'b') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'b') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'B'
-> ((x ~ 'B') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'B') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'B') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'c'
-> ((x ~ 'c') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'c') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'c') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'C'
-> ((x ~ 'C') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'C') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'C') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'd'
-> ((x ~ 'd') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'d') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'd') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'D'
-> ((x ~ 'D') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'D') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'D') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'e'
-> ((x ~ 'e') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'e') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'e') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'E'
-> ((x ~ 'E') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'E') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'E') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'f'
-> ((x ~ 'f') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'f') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'f') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'F'
-> ((x ~ 'F') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'F') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'F') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'g'
-> ((x ~ 'g') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'g') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'g') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'G'
-> ((x ~ 'G') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'G') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'G') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'h'
-> ((x ~ 'h') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'h') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'h') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'H'
-> ((x ~ 'H') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'H') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'H') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'i'
-> ((x ~ 'i') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'i') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'i') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'I'
-> ((x ~ 'I') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'I') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'I') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'j'
-> ((x ~ 'j') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'j') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'j') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'J'
-> ((x ~ 'J') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'J') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'J') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'k'
-> ((x ~ 'k') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'k') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'k') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'K'
-> ((x ~ 'K') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'K') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'K') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'l'
-> ((x ~ 'l') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'l') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'l') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'L'
-> ((x ~ 'L') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'L') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'L') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'm'
-> ((x ~ 'm') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'m') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'm') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'M'
-> ((x ~ 'M') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'M') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'M') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'n'
-> ((x ~ 'n') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'n') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'n') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'N'
-> ((x ~ 'N') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'N') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'N') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'o'
-> ((x ~ 'o') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'o') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'o') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'O'
-> ((x ~ 'O') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'O') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'O') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'p'
-> ((x ~ 'p') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'p') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'p') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'P'
-> ((x ~ 'P') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'P') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'P') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'q'
-> ((x ~ 'q') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'q') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'q') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'Q'
-> ((x ~ 'Q') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'Q') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'Q') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'r'
-> ((x ~ 'r') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'r') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'r') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'R'
-> ((x ~ 'R') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'R') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'R') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 's'
-> ((x ~ 's') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'s') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 's') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'S'
-> ((x ~ 'S') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'S') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'S') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 't'
-> ((x ~ 't') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'t') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 't') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'T'
-> ((x ~ 'T') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'T') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'T') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'u'
-> ((x ~ 'u') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'u') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'u') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'U'
-> ((x ~ 'U') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'U') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'U') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'v'
-> ((x ~ 'v') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'v') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'v') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'V'
-> ((x ~ 'V') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'V') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'V') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'w'
-> ((x ~ 'w') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'w') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'w') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'W'
-> ((x ~ 'W') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'W') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'W') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'x'
-> ((x ~ 'x') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'x') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'x') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'X'
-> ((x ~ 'X') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'X') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'X') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'y'
-> ((x ~ 'y') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'y') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'y') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'Y'
-> ((x ~ 'Y') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'Y') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'Y') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'z'
-> ((x ~ 'z') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'z') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'z') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'Z'
-> ((x ~ 'Z') => SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x)
-> SBool (IsAlphaSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'Z') SBool 'True
SBool (IsAlphaSym @@ x)
(x ~ 'Z') => SBool (IsAlphaSym @@ x)
STrue
    (SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x))
-> SBool (IsAlphaSym @@ x) -> SBool (IsAlphaSym @@ x)
forall a b. (a -> b) -> a -> b
$ SBool 'False -> SBool (IsAlpha x)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

instance SingChPred IsAlphaSym where singChPred :: Lam SChar SBool IsAlphaSym
singChPred = Lam SChar SBool IsAlphaSym
sIsAlphaSym

-- | @0-9A-Fa-f@
type IsHexDigit :: Char -> Bool
type family IsHexDigit ch where
    IsHexDigit '0' = True
    IsHexDigit '1' = True
    IsHexDigit '2' = True
    IsHexDigit '3' = True
    IsHexDigit '4' = True
    IsHexDigit '5' = True
    IsHexDigit '6' = True
    IsHexDigit '7' = True
    IsHexDigit '8' = True
    IsHexDigit '9' = True
    IsHexDigit 'a' = True
    IsHexDigit 'A' = True
    IsHexDigit 'b' = True
    IsHexDigit 'B' = True
    IsHexDigit 'c' = True
    IsHexDigit 'C' = True
    IsHexDigit 'd' = True
    IsHexDigit 'D' = True
    IsHexDigit 'e' = True
    IsHexDigit 'E' = True
    IsHexDigit 'f' = True
    IsHexDigit 'F' = True
    IsHexDigit _   = False

type IsHexDigitSym :: Char ~> Bool
data IsHexDigitSym ch
type instance App IsHexDigitSym ch = IsHexDigit ch

sIsHexDigitSym :: Lam SChar SBool IsHexDigitSym
sIsHexDigitSym :: Lam SChar SBool IsHexDigitSym
sIsHexDigitSym = LamRep SChar SBool IsHexDigitSym -> Lam SChar SBool IsHexDigitSym
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep SChar SBool IsHexDigitSym -> Lam SChar SBool IsHexDigitSym)
-> LamRep SChar SBool IsHexDigitSym
-> Lam SChar SBool IsHexDigitSym
forall a b. (a -> b) -> a -> b
$ \SChar x
ch ->
      SChar x
-> SChar '0'
-> ((x ~ '0') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'0') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ '0') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '1'
-> ((x ~ '1') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'1') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ '1') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '2'
-> ((x ~ '2') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'2') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ '2') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '3'
-> ((x ~ '3') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'3') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ '3') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '4'
-> ((x ~ '4') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'4') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ '4') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '5'
-> ((x ~ '5') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'5') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ '5') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '6'
-> ((x ~ '6') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'6') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ '6') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '7'
-> ((x ~ '7') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'7') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ '7') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '8'
-> ((x ~ '8') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'8') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ '8') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '9'
-> ((x ~ '9') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'9') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ '9') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'a'
-> ((x ~ 'a') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'a') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'a') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'A'
-> ((x ~ 'A') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'A') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'A') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'b'
-> ((x ~ 'b') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'b') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'b') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'B'
-> ((x ~ 'B') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'B') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'B') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'c'
-> ((x ~ 'c') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'c') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'c') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'C'
-> ((x ~ 'C') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'C') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'C') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'd'
-> ((x ~ 'd') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'d') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'd') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'D'
-> ((x ~ 'D') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'D') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'D') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'e'
-> ((x ~ 'e') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'e') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'e') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'E'
-> ((x ~ 'E') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'E') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'E') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'f'
-> ((x ~ 'f') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'f') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'f') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'F'
-> ((x ~ 'F') => SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x)
-> SBool (IsHexDigitSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'F') SBool 'True
SBool (IsHexDigitSym @@ x)
(x ~ 'F') => SBool (IsHexDigitSym @@ x)
STrue
    (SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x))
-> SBool (IsHexDigitSym @@ x) -> SBool (IsHexDigitSym @@ x)
forall a b. (a -> b) -> a -> b
$ SBool 'False -> SBool (IsHexDigit x)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

instance SingChPred IsHexDigitSym where singChPred :: Lam SChar SBool IsHexDigitSym
singChPred = Lam SChar SBool IsHexDigitSym
sIsHexDigitSym