singletons-base-3.4: tests/compile-and-dump/GradingClient/Database.golden
GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| data Nat
= Zero | Succ Nat
deriving (Eq, Ord) |]
======>
data Nat
= Zero | Succ Nat
deriving (Eq, Ord)
type ZeroSym0 :: Nat
type family ZeroSym0 :: Nat where
ZeroSym0 = Zero
type SuccSym0 :: (~>) Nat Nat
data SuccSym0 :: (~>) Nat Nat
where
SuccSym0KindInference :: SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
SuccSym0 a0123456789876543210
type instance Apply SuccSym0 a0123456789876543210 = Succ a0123456789876543210
instance SuppressUnusedWarnings SuccSym0 where
suppressUnusedWarnings = snd ((,) SuccSym0KindInference ())
type SuccSym1 :: Nat -> Nat
type family SuccSym1 (a0123456789876543210 :: Nat) :: Nat where
SuccSym1 a0123456789876543210 = Succ a0123456789876543210
type TFHelper_0123456789876543210 :: Nat -> Nat -> Bool
type family TFHelper_0123456789876543210 (a :: Nat) (a :: Nat) :: Bool where
TFHelper_0123456789876543210 Zero Zero = TrueSym0
TFHelper_0123456789876543210 Zero (Succ _) = FalseSym0
TFHelper_0123456789876543210 (Succ _) Zero = FalseSym0
TFHelper_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210
type TFHelper_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Bool)
data TFHelper_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Bool)
where
TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) =>
TFHelper_0123456789876543210Sym0 a0123456789876543210
type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym0KindInference ())
type TFHelper_0123456789876543210Sym1 :: Nat -> (~>) Nat Bool
data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: Nat) :: (~>) Nat Bool
where
TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) =>
TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym1KindInference ())
type TFHelper_0123456789876543210Sym2 :: Nat -> Nat -> Bool
type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Bool where
TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance PEq Nat where
type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
type Compare_0123456789876543210 :: Nat -> Nat -> Ordering
type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where
Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)
Compare_0123456789876543210 Zero (Succ _) = LTSym0
Compare_0123456789876543210 (Succ _) Zero = GTSym0
type Compare_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Ordering)
data Compare_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Ordering)
where
Compare_0123456789876543210Sym0KindInference :: SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
Compare_0123456789876543210Sym0 a0123456789876543210
type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) Compare_0123456789876543210Sym0KindInference ())
type Compare_0123456789876543210Sym1 :: Nat -> (~>) Nat Ordering
data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Nat) :: (~>) Nat Ordering
where
Compare_0123456789876543210Sym1KindInference :: SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) =>
Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) Compare_0123456789876543210Sym1KindInference ())
type Compare_0123456789876543210Sym2 :: Nat -> Nat -> Ordering
type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Ordering where
Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
instance POrd Nat where
type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
data SNat :: Nat -> Type
where
SZero :: SNat (Zero :: Nat)
SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat)
type instance Sing @Nat = SNat
instance SingKind Nat where
type Demote Nat = Nat
fromSing SZero = Zero
fromSing (SSucc b) = Succ (fromSing b)
toSing Zero = SomeSing SZero
toSing (Succ (b :: Demote Nat))
= case toSing b :: SomeSing Nat of SomeSing c -> SomeSing (SSucc c)
instance SEq Nat => SEq Nat where
(%==) ::
forall (t1 :: Nat) (t2 :: Nat). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun Nat ((~>) Nat Bool)
-> Type) t1) t2)
(%==) SZero SZero = STrue
(%==) SZero (SSucc _) = SFalse
(%==) (SSucc _) SZero = SFalse
(%==)
(SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
(SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
sB_0123456789876543210
instance SOrd Nat => SOrd Nat where
sCompare ::
forall (t1 :: Nat) (t2 :: Nat). Sing t1
-> Sing t2
-> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering)
-> Type) t1) t2)
sCompare SZero SZero
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
SNil
sCompare
(SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
(SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
SNil)
sCompare SZero (SSucc _) = SLT
sCompare (SSucc _) SZero = SGT
instance SDecide Nat => SDecide Nat where
(%~) SZero SZero = Proved Refl
(%~) SZero (SSucc _) = Disproved (\ x -> case x of {})
(%~) (SSucc _) SZero = Disproved (\ x -> case x of {})
(%~) (SSucc a) (SSucc b)
= case (%~) a b of
Proved Refl -> Proved Refl
Disproved contra
-> Disproved (\ refl -> case refl of Refl -> contra Refl)
instance Eq (SNat (z :: Nat)) where
(==) _ _ = True
instance SDecide Nat =>
GHC.Internal.Data.Type.Equality.TestEquality (SNat :: Nat
-> Type) where
GHC.Internal.Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance SDecide Nat =>
GHC.Internal.Data.Type.Coercion.TestCoercion (SNat :: Nat
-> Type) where
GHC.Internal.Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
instance Ord (SNat (z :: Nat)) where
compare _ _ = EQ
instance SingI Zero where
sing = SZero
instance SingI n => SingI (Succ (n :: Nat)) where
sing = SSucc sing
instance SingI1 Succ where
liftSing = SSucc
instance SingI (SuccSym0 :: (~>) Nat Nat) where
sing = singFun1 @SuccSym0 SSucc
GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| append :: Schema -> Schema -> Schema
append (Sch s1) (Sch s2) = Sch (s1 ++ s2)
attrNotIn :: Attribute -> Schema -> Bool
attrNotIn _ (Sch []) = True
attrNotIn (Attr name u) (Sch ((Attr name' _) : t))
= (name /= name') && (attrNotIn (Attr name u) (Sch t))
disjoint :: Schema -> Schema -> Bool
disjoint (Sch []) _ = True
disjoint (Sch (h : t)) s = (attrNotIn h s) && (disjoint (Sch t) s)
occurs :: [AChar] -> Schema -> Bool
occurs _ (Sch []) = False
occurs name (Sch ((Attr name' _) : attrs))
= name == name' || occurs name (Sch attrs)
lookup :: [AChar] -> Schema -> U
lookup _ (Sch []) = undefined
lookup name (Sch ((Attr name' u) : attrs))
= if name == name' then u else lookup name (Sch attrs)
data U
= BOOL | STRING | NAT | VEC U Nat
deriving (Read, Eq, Show)
data AChar
= CA |
CB |
CC |
CD |
CE |
CF |
CG |
CH |
CI |
CJ |
CK |
CL |
CM |
CN |
CO |
CP |
CQ |
CR |
CS |
CT |
CU |
CV |
CW |
CX |
CY |
CZ
deriving (Read, Show, Eq)
data Attribute = Attr [AChar] U
data Schema = Sch [Attribute] |]
======>
data U
= BOOL | STRING | NAT | VEC U Nat
deriving (Read, Eq, Show)
data AChar
= CA |
CB |
CC |
CD |
CE |
CF |
CG |
CH |
CI |
CJ |
CK |
CL |
CM |
CN |
CO |
CP |
CQ |
CR |
CS |
CT |
CU |
CV |
CW |
CX |
CY |
CZ
deriving (Read, Show, Eq)
data Attribute = Attr [AChar] U
data Schema = Sch [Attribute]
append :: Schema -> Schema -> Schema
append (Sch s1) (Sch s2) = Sch (s1 ++ s2)
attrNotIn :: Attribute -> Schema -> Bool
attrNotIn _ (Sch []) = True
attrNotIn (Attr name u) (Sch (Attr name' _ : t))
= ((name /= name') && attrNotIn (Attr name u) (Sch t))
disjoint :: Schema -> Schema -> Bool
disjoint (Sch []) _ = True
disjoint (Sch (h : t)) s = (attrNotIn h s && disjoint (Sch t) s)
occurs :: [AChar] -> Schema -> Bool
occurs _ (Sch []) = False
occurs name (Sch (Attr name' _ : attrs))
= ((name == name') || occurs name (Sch attrs))
lookup :: [AChar] -> Schema -> U
lookup _ (Sch []) = undefined
lookup name (Sch (Attr name' u : attrs))
= if (name == name') then u else lookup name (Sch attrs)
type BOOLSym0 :: U
type family BOOLSym0 :: U where
BOOLSym0 = BOOL
type STRINGSym0 :: U
type family STRINGSym0 :: U where
STRINGSym0 = STRING
type NATSym0 :: U
type family NATSym0 :: U where
NATSym0 = NAT
type VECSym0 :: (~>) U ((~>) Nat U)
data VECSym0 :: (~>) U ((~>) Nat U)
where
VECSym0KindInference :: SameKind (Apply VECSym0 arg) (VECSym1 arg) =>
VECSym0 a0123456789876543210
type instance Apply VECSym0 a0123456789876543210 = VECSym1 a0123456789876543210
instance SuppressUnusedWarnings VECSym0 where
suppressUnusedWarnings = snd ((,) VECSym0KindInference ())
type VECSym1 :: U -> (~>) Nat U
data VECSym1 (a0123456789876543210 :: U) :: (~>) Nat U
where
VECSym1KindInference :: SameKind (Apply (VECSym1 a0123456789876543210) arg) (VECSym2 a0123456789876543210 arg) =>
VECSym1 a0123456789876543210 a0123456789876543210
type instance Apply (VECSym1 a0123456789876543210) a0123456789876543210 = VEC a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (VECSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) VECSym1KindInference ())
type VECSym2 :: U -> Nat -> U
type family VECSym2 (a0123456789876543210 :: U) (a0123456789876543210 :: Nat) :: U where
VECSym2 a0123456789876543210 a0123456789876543210 = VEC a0123456789876543210 a0123456789876543210
type CASym0 :: AChar
type family CASym0 :: AChar where
CASym0 = CA
type CBSym0 :: AChar
type family CBSym0 :: AChar where
CBSym0 = CB
type CCSym0 :: AChar
type family CCSym0 :: AChar where
CCSym0 = CC
type CDSym0 :: AChar
type family CDSym0 :: AChar where
CDSym0 = CD
type CESym0 :: AChar
type family CESym0 :: AChar where
CESym0 = CE
type CFSym0 :: AChar
type family CFSym0 :: AChar where
CFSym0 = CF
type CGSym0 :: AChar
type family CGSym0 :: AChar where
CGSym0 = CG
type CHSym0 :: AChar
type family CHSym0 :: AChar where
CHSym0 = CH
type CISym0 :: AChar
type family CISym0 :: AChar where
CISym0 = CI
type CJSym0 :: AChar
type family CJSym0 :: AChar where
CJSym0 = CJ
type CKSym0 :: AChar
type family CKSym0 :: AChar where
CKSym0 = CK
type CLSym0 :: AChar
type family CLSym0 :: AChar where
CLSym0 = CL
type CMSym0 :: AChar
type family CMSym0 :: AChar where
CMSym0 = CM
type CNSym0 :: AChar
type family CNSym0 :: AChar where
CNSym0 = CN
type COSym0 :: AChar
type family COSym0 :: AChar where
COSym0 = CO
type CPSym0 :: AChar
type family CPSym0 :: AChar where
CPSym0 = CP
type CQSym0 :: AChar
type family CQSym0 :: AChar where
CQSym0 = CQ
type CRSym0 :: AChar
type family CRSym0 :: AChar where
CRSym0 = CR
type CSSym0 :: AChar
type family CSSym0 :: AChar where
CSSym0 = CS
type CTSym0 :: AChar
type family CTSym0 :: AChar where
CTSym0 = CT
type CUSym0 :: AChar
type family CUSym0 :: AChar where
CUSym0 = CU
type CVSym0 :: AChar
type family CVSym0 :: AChar where
CVSym0 = CV
type CWSym0 :: AChar
type family CWSym0 :: AChar where
CWSym0 = CW
type CXSym0 :: AChar
type family CXSym0 :: AChar where
CXSym0 = CX
type CYSym0 :: AChar
type family CYSym0 :: AChar where
CYSym0 = CY
type CZSym0 :: AChar
type family CZSym0 :: AChar where
CZSym0 = CZ
type AttrSym0 :: (~>) [AChar] ((~>) U Attribute)
data AttrSym0 :: (~>) [AChar] ((~>) U Attribute)
where
AttrSym0KindInference :: SameKind (Apply AttrSym0 arg) (AttrSym1 arg) =>
AttrSym0 a0123456789876543210
type instance Apply AttrSym0 a0123456789876543210 = AttrSym1 a0123456789876543210
instance SuppressUnusedWarnings AttrSym0 where
suppressUnusedWarnings = snd ((,) AttrSym0KindInference ())
type AttrSym1 :: [AChar] -> (~>) U Attribute
data AttrSym1 (a0123456789876543210 :: [AChar]) :: (~>) U Attribute
where
AttrSym1KindInference :: SameKind (Apply (AttrSym1 a0123456789876543210) arg) (AttrSym2 a0123456789876543210 arg) =>
AttrSym1 a0123456789876543210 a0123456789876543210
type instance Apply (AttrSym1 a0123456789876543210) a0123456789876543210 = Attr a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (AttrSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) AttrSym1KindInference ())
type AttrSym2 :: [AChar] -> U -> Attribute
type family AttrSym2 (a0123456789876543210 :: [AChar]) (a0123456789876543210 :: U) :: Attribute where
AttrSym2 a0123456789876543210 a0123456789876543210 = Attr a0123456789876543210 a0123456789876543210
type SchSym0 :: (~>) [Attribute] Schema
data SchSym0 :: (~>) [Attribute] Schema
where
SchSym0KindInference :: SameKind (Apply SchSym0 arg) (SchSym1 arg) =>
SchSym0 a0123456789876543210
type instance Apply SchSym0 a0123456789876543210 = Sch a0123456789876543210
instance SuppressUnusedWarnings SchSym0 where
suppressUnusedWarnings = snd ((,) SchSym0KindInference ())
type SchSym1 :: [Attribute] -> Schema
type family SchSym1 (a0123456789876543210 :: [Attribute]) :: Schema where
SchSym1 a0123456789876543210 = Sch a0123456789876543210
data Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210
type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210 name'0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210 name'0123456789876543210
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) name'0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210 u0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210 u0123456789876543210
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210) u0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210) where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym3KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) where
suppressUnusedWarnings
= snd
((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym3KindInference
())
type family Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where
Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
type family Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where
Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs = Apply (Apply (==@#@$) name) name'
type family Case_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 t where
Case_0123456789876543210 name name' u attrs 'True = u
Case_0123456789876543210 name name' u attrs 'False = Apply (Apply LookupSym0 name) (Apply SchSym0 attrs)
type LookupSym0 :: (~>) [AChar] ((~>) Schema U)
data LookupSym0 :: (~>) [AChar] ((~>) Schema U)
where
LookupSym0KindInference :: SameKind (Apply LookupSym0 arg) (LookupSym1 arg) =>
LookupSym0 a0123456789876543210
type instance Apply LookupSym0 a0123456789876543210 = LookupSym1 a0123456789876543210
instance SuppressUnusedWarnings LookupSym0 where
suppressUnusedWarnings = snd ((,) LookupSym0KindInference ())
type LookupSym1 :: [AChar] -> (~>) Schema U
data LookupSym1 (a0123456789876543210 :: [AChar]) :: (~>) Schema U
where
LookupSym1KindInference :: SameKind (Apply (LookupSym1 a0123456789876543210) arg) (LookupSym2 a0123456789876543210 arg) =>
LookupSym1 a0123456789876543210 a0123456789876543210
type instance Apply (LookupSym1 a0123456789876543210) a0123456789876543210 = Lookup a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (LookupSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) LookupSym1KindInference ())
type LookupSym2 :: [AChar] -> Schema -> U
type family LookupSym2 (a0123456789876543210 :: [AChar]) (a0123456789876543210 :: Schema) :: U where
LookupSym2 a0123456789876543210 a0123456789876543210 = Lookup a0123456789876543210 a0123456789876543210
type OccursSym0 :: (~>) [AChar] ((~>) Schema Bool)
data OccursSym0 :: (~>) [AChar] ((~>) Schema Bool)
where
OccursSym0KindInference :: SameKind (Apply OccursSym0 arg) (OccursSym1 arg) =>
OccursSym0 a0123456789876543210
type instance Apply OccursSym0 a0123456789876543210 = OccursSym1 a0123456789876543210
instance SuppressUnusedWarnings OccursSym0 where
suppressUnusedWarnings = snd ((,) OccursSym0KindInference ())
type OccursSym1 :: [AChar] -> (~>) Schema Bool
data OccursSym1 (a0123456789876543210 :: [AChar]) :: (~>) Schema Bool
where
OccursSym1KindInference :: SameKind (Apply (OccursSym1 a0123456789876543210) arg) (OccursSym2 a0123456789876543210 arg) =>
OccursSym1 a0123456789876543210 a0123456789876543210
type instance Apply (OccursSym1 a0123456789876543210) a0123456789876543210 = Occurs a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (OccursSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) OccursSym1KindInference ())
type OccursSym2 :: [AChar] -> Schema -> Bool
type family OccursSym2 (a0123456789876543210 :: [AChar]) (a0123456789876543210 :: Schema) :: Bool where
OccursSym2 a0123456789876543210 a0123456789876543210 = Occurs a0123456789876543210 a0123456789876543210
type DisjointSym0 :: (~>) Schema ((~>) Schema Bool)
data DisjointSym0 :: (~>) Schema ((~>) Schema Bool)
where
DisjointSym0KindInference :: SameKind (Apply DisjointSym0 arg) (DisjointSym1 arg) =>
DisjointSym0 a0123456789876543210
type instance Apply DisjointSym0 a0123456789876543210 = DisjointSym1 a0123456789876543210
instance SuppressUnusedWarnings DisjointSym0 where
suppressUnusedWarnings = snd ((,) DisjointSym0KindInference ())
type DisjointSym1 :: Schema -> (~>) Schema Bool
data DisjointSym1 (a0123456789876543210 :: Schema) :: (~>) Schema Bool
where
DisjointSym1KindInference :: SameKind (Apply (DisjointSym1 a0123456789876543210) arg) (DisjointSym2 a0123456789876543210 arg) =>
DisjointSym1 a0123456789876543210 a0123456789876543210
type instance Apply (DisjointSym1 a0123456789876543210) a0123456789876543210 = Disjoint a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (DisjointSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) DisjointSym1KindInference ())
type DisjointSym2 :: Schema -> Schema -> Bool
type family DisjointSym2 (a0123456789876543210 :: Schema) (a0123456789876543210 :: Schema) :: Bool where
DisjointSym2 a0123456789876543210 a0123456789876543210 = Disjoint a0123456789876543210 a0123456789876543210
type AttrNotInSym0 :: (~>) Attribute ((~>) Schema Bool)
data AttrNotInSym0 :: (~>) Attribute ((~>) Schema Bool)
where
AttrNotInSym0KindInference :: SameKind (Apply AttrNotInSym0 arg) (AttrNotInSym1 arg) =>
AttrNotInSym0 a0123456789876543210
type instance Apply AttrNotInSym0 a0123456789876543210 = AttrNotInSym1 a0123456789876543210
instance SuppressUnusedWarnings AttrNotInSym0 where
suppressUnusedWarnings = snd ((,) AttrNotInSym0KindInference ())
type AttrNotInSym1 :: Attribute -> (~>) Schema Bool
data AttrNotInSym1 (a0123456789876543210 :: Attribute) :: (~>) Schema Bool
where
AttrNotInSym1KindInference :: SameKind (Apply (AttrNotInSym1 a0123456789876543210) arg) (AttrNotInSym2 a0123456789876543210 arg) =>
AttrNotInSym1 a0123456789876543210 a0123456789876543210
type instance Apply (AttrNotInSym1 a0123456789876543210) a0123456789876543210 = AttrNotIn a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (AttrNotInSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) AttrNotInSym1KindInference ())
type AttrNotInSym2 :: Attribute -> Schema -> Bool
type family AttrNotInSym2 (a0123456789876543210 :: Attribute) (a0123456789876543210 :: Schema) :: Bool where
AttrNotInSym2 a0123456789876543210 a0123456789876543210 = AttrNotIn a0123456789876543210 a0123456789876543210
type AppendSym0 :: (~>) Schema ((~>) Schema Schema)
data AppendSym0 :: (~>) Schema ((~>) Schema Schema)
where
AppendSym0KindInference :: SameKind (Apply AppendSym0 arg) (AppendSym1 arg) =>
AppendSym0 a0123456789876543210
type instance Apply AppendSym0 a0123456789876543210 = AppendSym1 a0123456789876543210
instance SuppressUnusedWarnings AppendSym0 where
suppressUnusedWarnings = snd ((,) AppendSym0KindInference ())
type AppendSym1 :: Schema -> (~>) Schema Schema
data AppendSym1 (a0123456789876543210 :: Schema) :: (~>) Schema Schema
where
AppendSym1KindInference :: SameKind (Apply (AppendSym1 a0123456789876543210) arg) (AppendSym2 a0123456789876543210 arg) =>
AppendSym1 a0123456789876543210 a0123456789876543210
type instance Apply (AppendSym1 a0123456789876543210) a0123456789876543210 = Append a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (AppendSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) AppendSym1KindInference ())
type AppendSym2 :: Schema -> Schema -> Schema
type family AppendSym2 (a0123456789876543210 :: Schema) (a0123456789876543210 :: Schema) :: Schema where
AppendSym2 a0123456789876543210 a0123456789876543210 = Append a0123456789876543210 a0123456789876543210
type Lookup :: [AChar] -> Schema -> U
type family Lookup (a :: [AChar]) (a :: Schema) :: U where
Lookup _ (Sch '[]) = UndefinedSym0
Lookup name (Sch ('(:) (Attr name' u) attrs)) = Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs)
type Occurs :: [AChar] -> Schema -> Bool
type family Occurs (a :: [AChar]) (a :: Schema) :: Bool where
Occurs _ (Sch '[]) = FalseSym0
Occurs name (Sch ('(:) (Attr name' _) attrs)) = Apply (Apply (||@#@$) (Apply (Apply (==@#@$) name) name')) (Apply (Apply OccursSym0 name) (Apply SchSym0 attrs))
type Disjoint :: Schema -> Schema -> Bool
type family Disjoint (a :: Schema) (a :: Schema) :: Bool where
Disjoint (Sch '[]) _ = TrueSym0
Disjoint (Sch ('(:) h t)) s = Apply (Apply (&&@#@$) (Apply (Apply AttrNotInSym0 h) s)) (Apply (Apply DisjointSym0 (Apply SchSym0 t)) s)
type AttrNotIn :: Attribute -> Schema -> Bool
type family AttrNotIn (a :: Attribute) (a :: Schema) :: Bool where
AttrNotIn _ (Sch '[]) = TrueSym0
AttrNotIn (Attr name u) (Sch ('(:) (Attr name' _) t)) = Apply (Apply (&&@#@$) (Apply (Apply (/=@#@$) name) name')) (Apply (Apply AttrNotInSym0 (Apply (Apply AttrSym0 name) u)) (Apply SchSym0 t))
type Append :: Schema -> Schema -> Schema
type family Append (a :: Schema) (a :: Schema) :: Schema where
Append (Sch s1) (Sch s2) = Apply SchSym0 (Apply (Apply (++@#@$) s1) s2)
type TFHelper_0123456789876543210 :: U -> U -> Bool
type family TFHelper_0123456789876543210 (a :: U) (a :: U) :: Bool where
TFHelper_0123456789876543210 BOOL BOOL = TrueSym0
TFHelper_0123456789876543210 BOOL STRING = FalseSym0
TFHelper_0123456789876543210 BOOL NAT = FalseSym0
TFHelper_0123456789876543210 BOOL (VEC _ _) = FalseSym0
TFHelper_0123456789876543210 STRING BOOL = FalseSym0
TFHelper_0123456789876543210 STRING STRING = TrueSym0
TFHelper_0123456789876543210 STRING NAT = FalseSym0
TFHelper_0123456789876543210 STRING (VEC _ _) = FalseSym0
TFHelper_0123456789876543210 NAT BOOL = FalseSym0
TFHelper_0123456789876543210 NAT STRING = FalseSym0
TFHelper_0123456789876543210 NAT NAT = TrueSym0
TFHelper_0123456789876543210 NAT (VEC _ _) = FalseSym0
TFHelper_0123456789876543210 (VEC _ _) BOOL = FalseSym0
TFHelper_0123456789876543210 (VEC _ _) STRING = FalseSym0
TFHelper_0123456789876543210 (VEC _ _) NAT = FalseSym0
TFHelper_0123456789876543210 (VEC a_0123456789876543210 a_0123456789876543210) (VEC b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)
type TFHelper_0123456789876543210Sym0 :: (~>) U ((~>) U Bool)
data TFHelper_0123456789876543210Sym0 :: (~>) U ((~>) U Bool)
where
TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) =>
TFHelper_0123456789876543210Sym0 a0123456789876543210
type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym0KindInference ())
type TFHelper_0123456789876543210Sym1 :: U -> (~>) U Bool
data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: U) :: (~>) U Bool
where
TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) =>
TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym1KindInference ())
type TFHelper_0123456789876543210Sym2 :: U -> U -> Bool
type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: U) (a0123456789876543210 :: U) :: Bool where
TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance PEq U where
type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
-> U -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: U) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 _ BOOL a_0123456789876543210 = Apply (Apply ShowStringSym0 "BOOL") a_0123456789876543210
ShowsPrec_0123456789876543210 _ STRING a_0123456789876543210 = Apply (Apply ShowStringSym0 "STRING") a_0123456789876543210
ShowsPrec_0123456789876543210 _ NAT a_0123456789876543210 = Apply (Apply ShowStringSym0 "NAT") a_0123456789876543210
ShowsPrec_0123456789876543210 p_0123456789876543210 (VEC arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "VEC ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210
type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) U ((~>) Symbol Symbol))
data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) U ((~>) Symbol Symbol))
where
ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
ShowsPrec_0123456789876543210Sym0 a0123456789876543210
type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym0KindInference ())
type ShowsPrec_0123456789876543210Sym1 :: GHC.Num.Natural.Natural
-> (~>) U ((~>) Symbol Symbol)
data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) U ((~>) Symbol Symbol)
where
ShowsPrec_0123456789876543210Sym1KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>
ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym1KindInference ())
type ShowsPrec_0123456789876543210Sym2 :: GHC.Num.Natural.Natural
-> U -> (~>) Symbol Symbol
data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: U) :: (~>) Symbol Symbol
where
ShowsPrec_0123456789876543210Sym2KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ())
type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural
-> U -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: U) (a0123456789876543210 :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance PShow U where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
-> AChar -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: AChar) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 _ CA a_0123456789876543210 = Apply (Apply ShowStringSym0 "CA") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CB a_0123456789876543210 = Apply (Apply ShowStringSym0 "CB") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CC a_0123456789876543210 = Apply (Apply ShowStringSym0 "CC") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CD a_0123456789876543210 = Apply (Apply ShowStringSym0 "CD") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CE a_0123456789876543210 = Apply (Apply ShowStringSym0 "CE") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CF a_0123456789876543210 = Apply (Apply ShowStringSym0 "CF") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CG a_0123456789876543210 = Apply (Apply ShowStringSym0 "CG") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CH a_0123456789876543210 = Apply (Apply ShowStringSym0 "CH") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CI a_0123456789876543210 = Apply (Apply ShowStringSym0 "CI") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CJ a_0123456789876543210 = Apply (Apply ShowStringSym0 "CJ") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CK a_0123456789876543210 = Apply (Apply ShowStringSym0 "CK") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CL a_0123456789876543210 = Apply (Apply ShowStringSym0 "CL") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CM a_0123456789876543210 = Apply (Apply ShowStringSym0 "CM") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CN a_0123456789876543210 = Apply (Apply ShowStringSym0 "CN") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CO a_0123456789876543210 = Apply (Apply ShowStringSym0 "CO") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CP a_0123456789876543210 = Apply (Apply ShowStringSym0 "CP") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CQ a_0123456789876543210 = Apply (Apply ShowStringSym0 "CQ") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CR a_0123456789876543210 = Apply (Apply ShowStringSym0 "CR") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CS a_0123456789876543210 = Apply (Apply ShowStringSym0 "CS") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CT a_0123456789876543210 = Apply (Apply ShowStringSym0 "CT") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CU a_0123456789876543210 = Apply (Apply ShowStringSym0 "CU") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CV a_0123456789876543210 = Apply (Apply ShowStringSym0 "CV") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CW a_0123456789876543210 = Apply (Apply ShowStringSym0 "CW") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CX a_0123456789876543210 = Apply (Apply ShowStringSym0 "CX") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CY a_0123456789876543210 = Apply (Apply ShowStringSym0 "CY") a_0123456789876543210
ShowsPrec_0123456789876543210 _ CZ a_0123456789876543210 = Apply (Apply ShowStringSym0 "CZ") a_0123456789876543210
type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) AChar ((~>) Symbol Symbol))
data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) AChar ((~>) Symbol Symbol))
where
ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
ShowsPrec_0123456789876543210Sym0 a0123456789876543210
type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym0KindInference ())
type ShowsPrec_0123456789876543210Sym1 :: GHC.Num.Natural.Natural
-> (~>) AChar ((~>) Symbol Symbol)
data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) AChar ((~>) Symbol Symbol)
where
ShowsPrec_0123456789876543210Sym1KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>
ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym1KindInference ())
type ShowsPrec_0123456789876543210Sym2 :: GHC.Num.Natural.Natural
-> AChar -> (~>) Symbol Symbol
data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: AChar) :: (~>) Symbol Symbol
where
ShowsPrec_0123456789876543210Sym2KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ())
type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural
-> AChar -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: AChar) (a0123456789876543210 :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance PShow AChar where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
type TFHelper_0123456789876543210 :: AChar -> AChar -> Bool
type family TFHelper_0123456789876543210 (a :: AChar) (a :: AChar) :: Bool where
TFHelper_0123456789876543210 CA CA = TrueSym0
TFHelper_0123456789876543210 CA CB = FalseSym0
TFHelper_0123456789876543210 CA CC = FalseSym0
TFHelper_0123456789876543210 CA CD = FalseSym0
TFHelper_0123456789876543210 CA CE = FalseSym0
TFHelper_0123456789876543210 CA CF = FalseSym0
TFHelper_0123456789876543210 CA CG = FalseSym0
TFHelper_0123456789876543210 CA CH = FalseSym0
TFHelper_0123456789876543210 CA CI = FalseSym0
TFHelper_0123456789876543210 CA CJ = FalseSym0
TFHelper_0123456789876543210 CA CK = FalseSym0
TFHelper_0123456789876543210 CA CL = FalseSym0
TFHelper_0123456789876543210 CA CM = FalseSym0
TFHelper_0123456789876543210 CA CN = FalseSym0
TFHelper_0123456789876543210 CA CO = FalseSym0
TFHelper_0123456789876543210 CA CP = FalseSym0
TFHelper_0123456789876543210 CA CQ = FalseSym0
TFHelper_0123456789876543210 CA CR = FalseSym0
TFHelper_0123456789876543210 CA CS = FalseSym0
TFHelper_0123456789876543210 CA CT = FalseSym0
TFHelper_0123456789876543210 CA CU = FalseSym0
TFHelper_0123456789876543210 CA CV = FalseSym0
TFHelper_0123456789876543210 CA CW = FalseSym0
TFHelper_0123456789876543210 CA CX = FalseSym0
TFHelper_0123456789876543210 CA CY = FalseSym0
TFHelper_0123456789876543210 CA CZ = FalseSym0
TFHelper_0123456789876543210 CB CA = FalseSym0
TFHelper_0123456789876543210 CB CB = TrueSym0
TFHelper_0123456789876543210 CB CC = FalseSym0
TFHelper_0123456789876543210 CB CD = FalseSym0
TFHelper_0123456789876543210 CB CE = FalseSym0
TFHelper_0123456789876543210 CB CF = FalseSym0
TFHelper_0123456789876543210 CB CG = FalseSym0
TFHelper_0123456789876543210 CB CH = FalseSym0
TFHelper_0123456789876543210 CB CI = FalseSym0
TFHelper_0123456789876543210 CB CJ = FalseSym0
TFHelper_0123456789876543210 CB CK = FalseSym0
TFHelper_0123456789876543210 CB CL = FalseSym0
TFHelper_0123456789876543210 CB CM = FalseSym0
TFHelper_0123456789876543210 CB CN = FalseSym0
TFHelper_0123456789876543210 CB CO = FalseSym0
TFHelper_0123456789876543210 CB CP = FalseSym0
TFHelper_0123456789876543210 CB CQ = FalseSym0
TFHelper_0123456789876543210 CB CR = FalseSym0
TFHelper_0123456789876543210 CB CS = FalseSym0
TFHelper_0123456789876543210 CB CT = FalseSym0
TFHelper_0123456789876543210 CB CU = FalseSym0
TFHelper_0123456789876543210 CB CV = FalseSym0
TFHelper_0123456789876543210 CB CW = FalseSym0
TFHelper_0123456789876543210 CB CX = FalseSym0
TFHelper_0123456789876543210 CB CY = FalseSym0
TFHelper_0123456789876543210 CB CZ = FalseSym0
TFHelper_0123456789876543210 CC CA = FalseSym0
TFHelper_0123456789876543210 CC CB = FalseSym0
TFHelper_0123456789876543210 CC CC = TrueSym0
TFHelper_0123456789876543210 CC CD = FalseSym0
TFHelper_0123456789876543210 CC CE = FalseSym0
TFHelper_0123456789876543210 CC CF = FalseSym0
TFHelper_0123456789876543210 CC CG = FalseSym0
TFHelper_0123456789876543210 CC CH = FalseSym0
TFHelper_0123456789876543210 CC CI = FalseSym0
TFHelper_0123456789876543210 CC CJ = FalseSym0
TFHelper_0123456789876543210 CC CK = FalseSym0
TFHelper_0123456789876543210 CC CL = FalseSym0
TFHelper_0123456789876543210 CC CM = FalseSym0
TFHelper_0123456789876543210 CC CN = FalseSym0
TFHelper_0123456789876543210 CC CO = FalseSym0
TFHelper_0123456789876543210 CC CP = FalseSym0
TFHelper_0123456789876543210 CC CQ = FalseSym0
TFHelper_0123456789876543210 CC CR = FalseSym0
TFHelper_0123456789876543210 CC CS = FalseSym0
TFHelper_0123456789876543210 CC CT = FalseSym0
TFHelper_0123456789876543210 CC CU = FalseSym0
TFHelper_0123456789876543210 CC CV = FalseSym0
TFHelper_0123456789876543210 CC CW = FalseSym0
TFHelper_0123456789876543210 CC CX = FalseSym0
TFHelper_0123456789876543210 CC CY = FalseSym0
TFHelper_0123456789876543210 CC CZ = FalseSym0
TFHelper_0123456789876543210 CD CA = FalseSym0
TFHelper_0123456789876543210 CD CB = FalseSym0
TFHelper_0123456789876543210 CD CC = FalseSym0
TFHelper_0123456789876543210 CD CD = TrueSym0
TFHelper_0123456789876543210 CD CE = FalseSym0
TFHelper_0123456789876543210 CD CF = FalseSym0
TFHelper_0123456789876543210 CD CG = FalseSym0
TFHelper_0123456789876543210 CD CH = FalseSym0
TFHelper_0123456789876543210 CD CI = FalseSym0
TFHelper_0123456789876543210 CD CJ = FalseSym0
TFHelper_0123456789876543210 CD CK = FalseSym0
TFHelper_0123456789876543210 CD CL = FalseSym0
TFHelper_0123456789876543210 CD CM = FalseSym0
TFHelper_0123456789876543210 CD CN = FalseSym0
TFHelper_0123456789876543210 CD CO = FalseSym0
TFHelper_0123456789876543210 CD CP = FalseSym0
TFHelper_0123456789876543210 CD CQ = FalseSym0
TFHelper_0123456789876543210 CD CR = FalseSym0
TFHelper_0123456789876543210 CD CS = FalseSym0
TFHelper_0123456789876543210 CD CT = FalseSym0
TFHelper_0123456789876543210 CD CU = FalseSym0
TFHelper_0123456789876543210 CD CV = FalseSym0
TFHelper_0123456789876543210 CD CW = FalseSym0
TFHelper_0123456789876543210 CD CX = FalseSym0
TFHelper_0123456789876543210 CD CY = FalseSym0
TFHelper_0123456789876543210 CD CZ = FalseSym0
TFHelper_0123456789876543210 CE CA = FalseSym0
TFHelper_0123456789876543210 CE CB = FalseSym0
TFHelper_0123456789876543210 CE CC = FalseSym0
TFHelper_0123456789876543210 CE CD = FalseSym0
TFHelper_0123456789876543210 CE CE = TrueSym0
TFHelper_0123456789876543210 CE CF = FalseSym0
TFHelper_0123456789876543210 CE CG = FalseSym0
TFHelper_0123456789876543210 CE CH = FalseSym0
TFHelper_0123456789876543210 CE CI = FalseSym0
TFHelper_0123456789876543210 CE CJ = FalseSym0
TFHelper_0123456789876543210 CE CK = FalseSym0
TFHelper_0123456789876543210 CE CL = FalseSym0
TFHelper_0123456789876543210 CE CM = FalseSym0
TFHelper_0123456789876543210 CE CN = FalseSym0
TFHelper_0123456789876543210 CE CO = FalseSym0
TFHelper_0123456789876543210 CE CP = FalseSym0
TFHelper_0123456789876543210 CE CQ = FalseSym0
TFHelper_0123456789876543210 CE CR = FalseSym0
TFHelper_0123456789876543210 CE CS = FalseSym0
TFHelper_0123456789876543210 CE CT = FalseSym0
TFHelper_0123456789876543210 CE CU = FalseSym0
TFHelper_0123456789876543210 CE CV = FalseSym0
TFHelper_0123456789876543210 CE CW = FalseSym0
TFHelper_0123456789876543210 CE CX = FalseSym0
TFHelper_0123456789876543210 CE CY = FalseSym0
TFHelper_0123456789876543210 CE CZ = FalseSym0
TFHelper_0123456789876543210 CF CA = FalseSym0
TFHelper_0123456789876543210 CF CB = FalseSym0
TFHelper_0123456789876543210 CF CC = FalseSym0
TFHelper_0123456789876543210 CF CD = FalseSym0
TFHelper_0123456789876543210 CF CE = FalseSym0
TFHelper_0123456789876543210 CF CF = TrueSym0
TFHelper_0123456789876543210 CF CG = FalseSym0
TFHelper_0123456789876543210 CF CH = FalseSym0
TFHelper_0123456789876543210 CF CI = FalseSym0
TFHelper_0123456789876543210 CF CJ = FalseSym0
TFHelper_0123456789876543210 CF CK = FalseSym0
TFHelper_0123456789876543210 CF CL = FalseSym0
TFHelper_0123456789876543210 CF CM = FalseSym0
TFHelper_0123456789876543210 CF CN = FalseSym0
TFHelper_0123456789876543210 CF CO = FalseSym0
TFHelper_0123456789876543210 CF CP = FalseSym0
TFHelper_0123456789876543210 CF CQ = FalseSym0
TFHelper_0123456789876543210 CF CR = FalseSym0
TFHelper_0123456789876543210 CF CS = FalseSym0
TFHelper_0123456789876543210 CF CT = FalseSym0
TFHelper_0123456789876543210 CF CU = FalseSym0
TFHelper_0123456789876543210 CF CV = FalseSym0
TFHelper_0123456789876543210 CF CW = FalseSym0
TFHelper_0123456789876543210 CF CX = FalseSym0
TFHelper_0123456789876543210 CF CY = FalseSym0
TFHelper_0123456789876543210 CF CZ = FalseSym0
TFHelper_0123456789876543210 CG CA = FalseSym0
TFHelper_0123456789876543210 CG CB = FalseSym0
TFHelper_0123456789876543210 CG CC = FalseSym0
TFHelper_0123456789876543210 CG CD = FalseSym0
TFHelper_0123456789876543210 CG CE = FalseSym0
TFHelper_0123456789876543210 CG CF = FalseSym0
TFHelper_0123456789876543210 CG CG = TrueSym0
TFHelper_0123456789876543210 CG CH = FalseSym0
TFHelper_0123456789876543210 CG CI = FalseSym0
TFHelper_0123456789876543210 CG CJ = FalseSym0
TFHelper_0123456789876543210 CG CK = FalseSym0
TFHelper_0123456789876543210 CG CL = FalseSym0
TFHelper_0123456789876543210 CG CM = FalseSym0
TFHelper_0123456789876543210 CG CN = FalseSym0
TFHelper_0123456789876543210 CG CO = FalseSym0
TFHelper_0123456789876543210 CG CP = FalseSym0
TFHelper_0123456789876543210 CG CQ = FalseSym0
TFHelper_0123456789876543210 CG CR = FalseSym0
TFHelper_0123456789876543210 CG CS = FalseSym0
TFHelper_0123456789876543210 CG CT = FalseSym0
TFHelper_0123456789876543210 CG CU = FalseSym0
TFHelper_0123456789876543210 CG CV = FalseSym0
TFHelper_0123456789876543210 CG CW = FalseSym0
TFHelper_0123456789876543210 CG CX = FalseSym0
TFHelper_0123456789876543210 CG CY = FalseSym0
TFHelper_0123456789876543210 CG CZ = FalseSym0
TFHelper_0123456789876543210 CH CA = FalseSym0
TFHelper_0123456789876543210 CH CB = FalseSym0
TFHelper_0123456789876543210 CH CC = FalseSym0
TFHelper_0123456789876543210 CH CD = FalseSym0
TFHelper_0123456789876543210 CH CE = FalseSym0
TFHelper_0123456789876543210 CH CF = FalseSym0
TFHelper_0123456789876543210 CH CG = FalseSym0
TFHelper_0123456789876543210 CH CH = TrueSym0
TFHelper_0123456789876543210 CH CI = FalseSym0
TFHelper_0123456789876543210 CH CJ = FalseSym0
TFHelper_0123456789876543210 CH CK = FalseSym0
TFHelper_0123456789876543210 CH CL = FalseSym0
TFHelper_0123456789876543210 CH CM = FalseSym0
TFHelper_0123456789876543210 CH CN = FalseSym0
TFHelper_0123456789876543210 CH CO = FalseSym0
TFHelper_0123456789876543210 CH CP = FalseSym0
TFHelper_0123456789876543210 CH CQ = FalseSym0
TFHelper_0123456789876543210 CH CR = FalseSym0
TFHelper_0123456789876543210 CH CS = FalseSym0
TFHelper_0123456789876543210 CH CT = FalseSym0
TFHelper_0123456789876543210 CH CU = FalseSym0
TFHelper_0123456789876543210 CH CV = FalseSym0
TFHelper_0123456789876543210 CH CW = FalseSym0
TFHelper_0123456789876543210 CH CX = FalseSym0
TFHelper_0123456789876543210 CH CY = FalseSym0
TFHelper_0123456789876543210 CH CZ = FalseSym0
TFHelper_0123456789876543210 CI CA = FalseSym0
TFHelper_0123456789876543210 CI CB = FalseSym0
TFHelper_0123456789876543210 CI CC = FalseSym0
TFHelper_0123456789876543210 CI CD = FalseSym0
TFHelper_0123456789876543210 CI CE = FalseSym0
TFHelper_0123456789876543210 CI CF = FalseSym0
TFHelper_0123456789876543210 CI CG = FalseSym0
TFHelper_0123456789876543210 CI CH = FalseSym0
TFHelper_0123456789876543210 CI CI = TrueSym0
TFHelper_0123456789876543210 CI CJ = FalseSym0
TFHelper_0123456789876543210 CI CK = FalseSym0
TFHelper_0123456789876543210 CI CL = FalseSym0
TFHelper_0123456789876543210 CI CM = FalseSym0
TFHelper_0123456789876543210 CI CN = FalseSym0
TFHelper_0123456789876543210 CI CO = FalseSym0
TFHelper_0123456789876543210 CI CP = FalseSym0
TFHelper_0123456789876543210 CI CQ = FalseSym0
TFHelper_0123456789876543210 CI CR = FalseSym0
TFHelper_0123456789876543210 CI CS = FalseSym0
TFHelper_0123456789876543210 CI CT = FalseSym0
TFHelper_0123456789876543210 CI CU = FalseSym0
TFHelper_0123456789876543210 CI CV = FalseSym0
TFHelper_0123456789876543210 CI CW = FalseSym0
TFHelper_0123456789876543210 CI CX = FalseSym0
TFHelper_0123456789876543210 CI CY = FalseSym0
TFHelper_0123456789876543210 CI CZ = FalseSym0
TFHelper_0123456789876543210 CJ CA = FalseSym0
TFHelper_0123456789876543210 CJ CB = FalseSym0
TFHelper_0123456789876543210 CJ CC = FalseSym0
TFHelper_0123456789876543210 CJ CD = FalseSym0
TFHelper_0123456789876543210 CJ CE = FalseSym0
TFHelper_0123456789876543210 CJ CF = FalseSym0
TFHelper_0123456789876543210 CJ CG = FalseSym0
TFHelper_0123456789876543210 CJ CH = FalseSym0
TFHelper_0123456789876543210 CJ CI = FalseSym0
TFHelper_0123456789876543210 CJ CJ = TrueSym0
TFHelper_0123456789876543210 CJ CK = FalseSym0
TFHelper_0123456789876543210 CJ CL = FalseSym0
TFHelper_0123456789876543210 CJ CM = FalseSym0
TFHelper_0123456789876543210 CJ CN = FalseSym0
TFHelper_0123456789876543210 CJ CO = FalseSym0
TFHelper_0123456789876543210 CJ CP = FalseSym0
TFHelper_0123456789876543210 CJ CQ = FalseSym0
TFHelper_0123456789876543210 CJ CR = FalseSym0
TFHelper_0123456789876543210 CJ CS = FalseSym0
TFHelper_0123456789876543210 CJ CT = FalseSym0
TFHelper_0123456789876543210 CJ CU = FalseSym0
TFHelper_0123456789876543210 CJ CV = FalseSym0
TFHelper_0123456789876543210 CJ CW = FalseSym0
TFHelper_0123456789876543210 CJ CX = FalseSym0
TFHelper_0123456789876543210 CJ CY = FalseSym0
TFHelper_0123456789876543210 CJ CZ = FalseSym0
TFHelper_0123456789876543210 CK CA = FalseSym0
TFHelper_0123456789876543210 CK CB = FalseSym0
TFHelper_0123456789876543210 CK CC = FalseSym0
TFHelper_0123456789876543210 CK CD = FalseSym0
TFHelper_0123456789876543210 CK CE = FalseSym0
TFHelper_0123456789876543210 CK CF = FalseSym0
TFHelper_0123456789876543210 CK CG = FalseSym0
TFHelper_0123456789876543210 CK CH = FalseSym0
TFHelper_0123456789876543210 CK CI = FalseSym0
TFHelper_0123456789876543210 CK CJ = FalseSym0
TFHelper_0123456789876543210 CK CK = TrueSym0
TFHelper_0123456789876543210 CK CL = FalseSym0
TFHelper_0123456789876543210 CK CM = FalseSym0
TFHelper_0123456789876543210 CK CN = FalseSym0
TFHelper_0123456789876543210 CK CO = FalseSym0
TFHelper_0123456789876543210 CK CP = FalseSym0
TFHelper_0123456789876543210 CK CQ = FalseSym0
TFHelper_0123456789876543210 CK CR = FalseSym0
TFHelper_0123456789876543210 CK CS = FalseSym0
TFHelper_0123456789876543210 CK CT = FalseSym0
TFHelper_0123456789876543210 CK CU = FalseSym0
TFHelper_0123456789876543210 CK CV = FalseSym0
TFHelper_0123456789876543210 CK CW = FalseSym0
TFHelper_0123456789876543210 CK CX = FalseSym0
TFHelper_0123456789876543210 CK CY = FalseSym0
TFHelper_0123456789876543210 CK CZ = FalseSym0
TFHelper_0123456789876543210 CL CA = FalseSym0
TFHelper_0123456789876543210 CL CB = FalseSym0
TFHelper_0123456789876543210 CL CC = FalseSym0
TFHelper_0123456789876543210 CL CD = FalseSym0
TFHelper_0123456789876543210 CL CE = FalseSym0
TFHelper_0123456789876543210 CL CF = FalseSym0
TFHelper_0123456789876543210 CL CG = FalseSym0
TFHelper_0123456789876543210 CL CH = FalseSym0
TFHelper_0123456789876543210 CL CI = FalseSym0
TFHelper_0123456789876543210 CL CJ = FalseSym0
TFHelper_0123456789876543210 CL CK = FalseSym0
TFHelper_0123456789876543210 CL CL = TrueSym0
TFHelper_0123456789876543210 CL CM = FalseSym0
TFHelper_0123456789876543210 CL CN = FalseSym0
TFHelper_0123456789876543210 CL CO = FalseSym0
TFHelper_0123456789876543210 CL CP = FalseSym0
TFHelper_0123456789876543210 CL CQ = FalseSym0
TFHelper_0123456789876543210 CL CR = FalseSym0
TFHelper_0123456789876543210 CL CS = FalseSym0
TFHelper_0123456789876543210 CL CT = FalseSym0
TFHelper_0123456789876543210 CL CU = FalseSym0
TFHelper_0123456789876543210 CL CV = FalseSym0
TFHelper_0123456789876543210 CL CW = FalseSym0
TFHelper_0123456789876543210 CL CX = FalseSym0
TFHelper_0123456789876543210 CL CY = FalseSym0
TFHelper_0123456789876543210 CL CZ = FalseSym0
TFHelper_0123456789876543210 CM CA = FalseSym0
TFHelper_0123456789876543210 CM CB = FalseSym0
TFHelper_0123456789876543210 CM CC = FalseSym0
TFHelper_0123456789876543210 CM CD = FalseSym0
TFHelper_0123456789876543210 CM CE = FalseSym0
TFHelper_0123456789876543210 CM CF = FalseSym0
TFHelper_0123456789876543210 CM CG = FalseSym0
TFHelper_0123456789876543210 CM CH = FalseSym0
TFHelper_0123456789876543210 CM CI = FalseSym0
TFHelper_0123456789876543210 CM CJ = FalseSym0
TFHelper_0123456789876543210 CM CK = FalseSym0
TFHelper_0123456789876543210 CM CL = FalseSym0
TFHelper_0123456789876543210 CM CM = TrueSym0
TFHelper_0123456789876543210 CM CN = FalseSym0
TFHelper_0123456789876543210 CM CO = FalseSym0
TFHelper_0123456789876543210 CM CP = FalseSym0
TFHelper_0123456789876543210 CM CQ = FalseSym0
TFHelper_0123456789876543210 CM CR = FalseSym0
TFHelper_0123456789876543210 CM CS = FalseSym0
TFHelper_0123456789876543210 CM CT = FalseSym0
TFHelper_0123456789876543210 CM CU = FalseSym0
TFHelper_0123456789876543210 CM CV = FalseSym0
TFHelper_0123456789876543210 CM CW = FalseSym0
TFHelper_0123456789876543210 CM CX = FalseSym0
TFHelper_0123456789876543210 CM CY = FalseSym0
TFHelper_0123456789876543210 CM CZ = FalseSym0
TFHelper_0123456789876543210 CN CA = FalseSym0
TFHelper_0123456789876543210 CN CB = FalseSym0
TFHelper_0123456789876543210 CN CC = FalseSym0
TFHelper_0123456789876543210 CN CD = FalseSym0
TFHelper_0123456789876543210 CN CE = FalseSym0
TFHelper_0123456789876543210 CN CF = FalseSym0
TFHelper_0123456789876543210 CN CG = FalseSym0
TFHelper_0123456789876543210 CN CH = FalseSym0
TFHelper_0123456789876543210 CN CI = FalseSym0
TFHelper_0123456789876543210 CN CJ = FalseSym0
TFHelper_0123456789876543210 CN CK = FalseSym0
TFHelper_0123456789876543210 CN CL = FalseSym0
TFHelper_0123456789876543210 CN CM = FalseSym0
TFHelper_0123456789876543210 CN CN = TrueSym0
TFHelper_0123456789876543210 CN CO = FalseSym0
TFHelper_0123456789876543210 CN CP = FalseSym0
TFHelper_0123456789876543210 CN CQ = FalseSym0
TFHelper_0123456789876543210 CN CR = FalseSym0
TFHelper_0123456789876543210 CN CS = FalseSym0
TFHelper_0123456789876543210 CN CT = FalseSym0
TFHelper_0123456789876543210 CN CU = FalseSym0
TFHelper_0123456789876543210 CN CV = FalseSym0
TFHelper_0123456789876543210 CN CW = FalseSym0
TFHelper_0123456789876543210 CN CX = FalseSym0
TFHelper_0123456789876543210 CN CY = FalseSym0
TFHelper_0123456789876543210 CN CZ = FalseSym0
TFHelper_0123456789876543210 CO CA = FalseSym0
TFHelper_0123456789876543210 CO CB = FalseSym0
TFHelper_0123456789876543210 CO CC = FalseSym0
TFHelper_0123456789876543210 CO CD = FalseSym0
TFHelper_0123456789876543210 CO CE = FalseSym0
TFHelper_0123456789876543210 CO CF = FalseSym0
TFHelper_0123456789876543210 CO CG = FalseSym0
TFHelper_0123456789876543210 CO CH = FalseSym0
TFHelper_0123456789876543210 CO CI = FalseSym0
TFHelper_0123456789876543210 CO CJ = FalseSym0
TFHelper_0123456789876543210 CO CK = FalseSym0
TFHelper_0123456789876543210 CO CL = FalseSym0
TFHelper_0123456789876543210 CO CM = FalseSym0
TFHelper_0123456789876543210 CO CN = FalseSym0
TFHelper_0123456789876543210 CO CO = TrueSym0
TFHelper_0123456789876543210 CO CP = FalseSym0
TFHelper_0123456789876543210 CO CQ = FalseSym0
TFHelper_0123456789876543210 CO CR = FalseSym0
TFHelper_0123456789876543210 CO CS = FalseSym0
TFHelper_0123456789876543210 CO CT = FalseSym0
TFHelper_0123456789876543210 CO CU = FalseSym0
TFHelper_0123456789876543210 CO CV = FalseSym0
TFHelper_0123456789876543210 CO CW = FalseSym0
TFHelper_0123456789876543210 CO CX = FalseSym0
TFHelper_0123456789876543210 CO CY = FalseSym0
TFHelper_0123456789876543210 CO CZ = FalseSym0
TFHelper_0123456789876543210 CP CA = FalseSym0
TFHelper_0123456789876543210 CP CB = FalseSym0
TFHelper_0123456789876543210 CP CC = FalseSym0
TFHelper_0123456789876543210 CP CD = FalseSym0
TFHelper_0123456789876543210 CP CE = FalseSym0
TFHelper_0123456789876543210 CP CF = FalseSym0
TFHelper_0123456789876543210 CP CG = FalseSym0
TFHelper_0123456789876543210 CP CH = FalseSym0
TFHelper_0123456789876543210 CP CI = FalseSym0
TFHelper_0123456789876543210 CP CJ = FalseSym0
TFHelper_0123456789876543210 CP CK = FalseSym0
TFHelper_0123456789876543210 CP CL = FalseSym0
TFHelper_0123456789876543210 CP CM = FalseSym0
TFHelper_0123456789876543210 CP CN = FalseSym0
TFHelper_0123456789876543210 CP CO = FalseSym0
TFHelper_0123456789876543210 CP CP = TrueSym0
TFHelper_0123456789876543210 CP CQ = FalseSym0
TFHelper_0123456789876543210 CP CR = FalseSym0
TFHelper_0123456789876543210 CP CS = FalseSym0
TFHelper_0123456789876543210 CP CT = FalseSym0
TFHelper_0123456789876543210 CP CU = FalseSym0
TFHelper_0123456789876543210 CP CV = FalseSym0
TFHelper_0123456789876543210 CP CW = FalseSym0
TFHelper_0123456789876543210 CP CX = FalseSym0
TFHelper_0123456789876543210 CP CY = FalseSym0
TFHelper_0123456789876543210 CP CZ = FalseSym0
TFHelper_0123456789876543210 CQ CA = FalseSym0
TFHelper_0123456789876543210 CQ CB = FalseSym0
TFHelper_0123456789876543210 CQ CC = FalseSym0
TFHelper_0123456789876543210 CQ CD = FalseSym0
TFHelper_0123456789876543210 CQ CE = FalseSym0
TFHelper_0123456789876543210 CQ CF = FalseSym0
TFHelper_0123456789876543210 CQ CG = FalseSym0
TFHelper_0123456789876543210 CQ CH = FalseSym0
TFHelper_0123456789876543210 CQ CI = FalseSym0
TFHelper_0123456789876543210 CQ CJ = FalseSym0
TFHelper_0123456789876543210 CQ CK = FalseSym0
TFHelper_0123456789876543210 CQ CL = FalseSym0
TFHelper_0123456789876543210 CQ CM = FalseSym0
TFHelper_0123456789876543210 CQ CN = FalseSym0
TFHelper_0123456789876543210 CQ CO = FalseSym0
TFHelper_0123456789876543210 CQ CP = FalseSym0
TFHelper_0123456789876543210 CQ CQ = TrueSym0
TFHelper_0123456789876543210 CQ CR = FalseSym0
TFHelper_0123456789876543210 CQ CS = FalseSym0
TFHelper_0123456789876543210 CQ CT = FalseSym0
TFHelper_0123456789876543210 CQ CU = FalseSym0
TFHelper_0123456789876543210 CQ CV = FalseSym0
TFHelper_0123456789876543210 CQ CW = FalseSym0
TFHelper_0123456789876543210 CQ CX = FalseSym0
TFHelper_0123456789876543210 CQ CY = FalseSym0
TFHelper_0123456789876543210 CQ CZ = FalseSym0
TFHelper_0123456789876543210 CR CA = FalseSym0
TFHelper_0123456789876543210 CR CB = FalseSym0
TFHelper_0123456789876543210 CR CC = FalseSym0
TFHelper_0123456789876543210 CR CD = FalseSym0
TFHelper_0123456789876543210 CR CE = FalseSym0
TFHelper_0123456789876543210 CR CF = FalseSym0
TFHelper_0123456789876543210 CR CG = FalseSym0
TFHelper_0123456789876543210 CR CH = FalseSym0
TFHelper_0123456789876543210 CR CI = FalseSym0
TFHelper_0123456789876543210 CR CJ = FalseSym0
TFHelper_0123456789876543210 CR CK = FalseSym0
TFHelper_0123456789876543210 CR CL = FalseSym0
TFHelper_0123456789876543210 CR CM = FalseSym0
TFHelper_0123456789876543210 CR CN = FalseSym0
TFHelper_0123456789876543210 CR CO = FalseSym0
TFHelper_0123456789876543210 CR CP = FalseSym0
TFHelper_0123456789876543210 CR CQ = FalseSym0
TFHelper_0123456789876543210 CR CR = TrueSym0
TFHelper_0123456789876543210 CR CS = FalseSym0
TFHelper_0123456789876543210 CR CT = FalseSym0
TFHelper_0123456789876543210 CR CU = FalseSym0
TFHelper_0123456789876543210 CR CV = FalseSym0
TFHelper_0123456789876543210 CR CW = FalseSym0
TFHelper_0123456789876543210 CR CX = FalseSym0
TFHelper_0123456789876543210 CR CY = FalseSym0
TFHelper_0123456789876543210 CR CZ = FalseSym0
TFHelper_0123456789876543210 CS CA = FalseSym0
TFHelper_0123456789876543210 CS CB = FalseSym0
TFHelper_0123456789876543210 CS CC = FalseSym0
TFHelper_0123456789876543210 CS CD = FalseSym0
TFHelper_0123456789876543210 CS CE = FalseSym0
TFHelper_0123456789876543210 CS CF = FalseSym0
TFHelper_0123456789876543210 CS CG = FalseSym0
TFHelper_0123456789876543210 CS CH = FalseSym0
TFHelper_0123456789876543210 CS CI = FalseSym0
TFHelper_0123456789876543210 CS CJ = FalseSym0
TFHelper_0123456789876543210 CS CK = FalseSym0
TFHelper_0123456789876543210 CS CL = FalseSym0
TFHelper_0123456789876543210 CS CM = FalseSym0
TFHelper_0123456789876543210 CS CN = FalseSym0
TFHelper_0123456789876543210 CS CO = FalseSym0
TFHelper_0123456789876543210 CS CP = FalseSym0
TFHelper_0123456789876543210 CS CQ = FalseSym0
TFHelper_0123456789876543210 CS CR = FalseSym0
TFHelper_0123456789876543210 CS CS = TrueSym0
TFHelper_0123456789876543210 CS CT = FalseSym0
TFHelper_0123456789876543210 CS CU = FalseSym0
TFHelper_0123456789876543210 CS CV = FalseSym0
TFHelper_0123456789876543210 CS CW = FalseSym0
TFHelper_0123456789876543210 CS CX = FalseSym0
TFHelper_0123456789876543210 CS CY = FalseSym0
TFHelper_0123456789876543210 CS CZ = FalseSym0
TFHelper_0123456789876543210 CT CA = FalseSym0
TFHelper_0123456789876543210 CT CB = FalseSym0
TFHelper_0123456789876543210 CT CC = FalseSym0
TFHelper_0123456789876543210 CT CD = FalseSym0
TFHelper_0123456789876543210 CT CE = FalseSym0
TFHelper_0123456789876543210 CT CF = FalseSym0
TFHelper_0123456789876543210 CT CG = FalseSym0
TFHelper_0123456789876543210 CT CH = FalseSym0
TFHelper_0123456789876543210 CT CI = FalseSym0
TFHelper_0123456789876543210 CT CJ = FalseSym0
TFHelper_0123456789876543210 CT CK = FalseSym0
TFHelper_0123456789876543210 CT CL = FalseSym0
TFHelper_0123456789876543210 CT CM = FalseSym0
TFHelper_0123456789876543210 CT CN = FalseSym0
TFHelper_0123456789876543210 CT CO = FalseSym0
TFHelper_0123456789876543210 CT CP = FalseSym0
TFHelper_0123456789876543210 CT CQ = FalseSym0
TFHelper_0123456789876543210 CT CR = FalseSym0
TFHelper_0123456789876543210 CT CS = FalseSym0
TFHelper_0123456789876543210 CT CT = TrueSym0
TFHelper_0123456789876543210 CT CU = FalseSym0
TFHelper_0123456789876543210 CT CV = FalseSym0
TFHelper_0123456789876543210 CT CW = FalseSym0
TFHelper_0123456789876543210 CT CX = FalseSym0
TFHelper_0123456789876543210 CT CY = FalseSym0
TFHelper_0123456789876543210 CT CZ = FalseSym0
TFHelper_0123456789876543210 CU CA = FalseSym0
TFHelper_0123456789876543210 CU CB = FalseSym0
TFHelper_0123456789876543210 CU CC = FalseSym0
TFHelper_0123456789876543210 CU CD = FalseSym0
TFHelper_0123456789876543210 CU CE = FalseSym0
TFHelper_0123456789876543210 CU CF = FalseSym0
TFHelper_0123456789876543210 CU CG = FalseSym0
TFHelper_0123456789876543210 CU CH = FalseSym0
TFHelper_0123456789876543210 CU CI = FalseSym0
TFHelper_0123456789876543210 CU CJ = FalseSym0
TFHelper_0123456789876543210 CU CK = FalseSym0
TFHelper_0123456789876543210 CU CL = FalseSym0
TFHelper_0123456789876543210 CU CM = FalseSym0
TFHelper_0123456789876543210 CU CN = FalseSym0
TFHelper_0123456789876543210 CU CO = FalseSym0
TFHelper_0123456789876543210 CU CP = FalseSym0
TFHelper_0123456789876543210 CU CQ = FalseSym0
TFHelper_0123456789876543210 CU CR = FalseSym0
TFHelper_0123456789876543210 CU CS = FalseSym0
TFHelper_0123456789876543210 CU CT = FalseSym0
TFHelper_0123456789876543210 CU CU = TrueSym0
TFHelper_0123456789876543210 CU CV = FalseSym0
TFHelper_0123456789876543210 CU CW = FalseSym0
TFHelper_0123456789876543210 CU CX = FalseSym0
TFHelper_0123456789876543210 CU CY = FalseSym0
TFHelper_0123456789876543210 CU CZ = FalseSym0
TFHelper_0123456789876543210 CV CA = FalseSym0
TFHelper_0123456789876543210 CV CB = FalseSym0
TFHelper_0123456789876543210 CV CC = FalseSym0
TFHelper_0123456789876543210 CV CD = FalseSym0
TFHelper_0123456789876543210 CV CE = FalseSym0
TFHelper_0123456789876543210 CV CF = FalseSym0
TFHelper_0123456789876543210 CV CG = FalseSym0
TFHelper_0123456789876543210 CV CH = FalseSym0
TFHelper_0123456789876543210 CV CI = FalseSym0
TFHelper_0123456789876543210 CV CJ = FalseSym0
TFHelper_0123456789876543210 CV CK = FalseSym0
TFHelper_0123456789876543210 CV CL = FalseSym0
TFHelper_0123456789876543210 CV CM = FalseSym0
TFHelper_0123456789876543210 CV CN = FalseSym0
TFHelper_0123456789876543210 CV CO = FalseSym0
TFHelper_0123456789876543210 CV CP = FalseSym0
TFHelper_0123456789876543210 CV CQ = FalseSym0
TFHelper_0123456789876543210 CV CR = FalseSym0
TFHelper_0123456789876543210 CV CS = FalseSym0
TFHelper_0123456789876543210 CV CT = FalseSym0
TFHelper_0123456789876543210 CV CU = FalseSym0
TFHelper_0123456789876543210 CV CV = TrueSym0
TFHelper_0123456789876543210 CV CW = FalseSym0
TFHelper_0123456789876543210 CV CX = FalseSym0
TFHelper_0123456789876543210 CV CY = FalseSym0
TFHelper_0123456789876543210 CV CZ = FalseSym0
TFHelper_0123456789876543210 CW CA = FalseSym0
TFHelper_0123456789876543210 CW CB = FalseSym0
TFHelper_0123456789876543210 CW CC = FalseSym0
TFHelper_0123456789876543210 CW CD = FalseSym0
TFHelper_0123456789876543210 CW CE = FalseSym0
TFHelper_0123456789876543210 CW CF = FalseSym0
TFHelper_0123456789876543210 CW CG = FalseSym0
TFHelper_0123456789876543210 CW CH = FalseSym0
TFHelper_0123456789876543210 CW CI = FalseSym0
TFHelper_0123456789876543210 CW CJ = FalseSym0
TFHelper_0123456789876543210 CW CK = FalseSym0
TFHelper_0123456789876543210 CW CL = FalseSym0
TFHelper_0123456789876543210 CW CM = FalseSym0
TFHelper_0123456789876543210 CW CN = FalseSym0
TFHelper_0123456789876543210 CW CO = FalseSym0
TFHelper_0123456789876543210 CW CP = FalseSym0
TFHelper_0123456789876543210 CW CQ = FalseSym0
TFHelper_0123456789876543210 CW CR = FalseSym0
TFHelper_0123456789876543210 CW CS = FalseSym0
TFHelper_0123456789876543210 CW CT = FalseSym0
TFHelper_0123456789876543210 CW CU = FalseSym0
TFHelper_0123456789876543210 CW CV = FalseSym0
TFHelper_0123456789876543210 CW CW = TrueSym0
TFHelper_0123456789876543210 CW CX = FalseSym0
TFHelper_0123456789876543210 CW CY = FalseSym0
TFHelper_0123456789876543210 CW CZ = FalseSym0
TFHelper_0123456789876543210 CX CA = FalseSym0
TFHelper_0123456789876543210 CX CB = FalseSym0
TFHelper_0123456789876543210 CX CC = FalseSym0
TFHelper_0123456789876543210 CX CD = FalseSym0
TFHelper_0123456789876543210 CX CE = FalseSym0
TFHelper_0123456789876543210 CX CF = FalseSym0
TFHelper_0123456789876543210 CX CG = FalseSym0
TFHelper_0123456789876543210 CX CH = FalseSym0
TFHelper_0123456789876543210 CX CI = FalseSym0
TFHelper_0123456789876543210 CX CJ = FalseSym0
TFHelper_0123456789876543210 CX CK = FalseSym0
TFHelper_0123456789876543210 CX CL = FalseSym0
TFHelper_0123456789876543210 CX CM = FalseSym0
TFHelper_0123456789876543210 CX CN = FalseSym0
TFHelper_0123456789876543210 CX CO = FalseSym0
TFHelper_0123456789876543210 CX CP = FalseSym0
TFHelper_0123456789876543210 CX CQ = FalseSym0
TFHelper_0123456789876543210 CX CR = FalseSym0
TFHelper_0123456789876543210 CX CS = FalseSym0
TFHelper_0123456789876543210 CX CT = FalseSym0
TFHelper_0123456789876543210 CX CU = FalseSym0
TFHelper_0123456789876543210 CX CV = FalseSym0
TFHelper_0123456789876543210 CX CW = FalseSym0
TFHelper_0123456789876543210 CX CX = TrueSym0
TFHelper_0123456789876543210 CX CY = FalseSym0
TFHelper_0123456789876543210 CX CZ = FalseSym0
TFHelper_0123456789876543210 CY CA = FalseSym0
TFHelper_0123456789876543210 CY CB = FalseSym0
TFHelper_0123456789876543210 CY CC = FalseSym0
TFHelper_0123456789876543210 CY CD = FalseSym0
TFHelper_0123456789876543210 CY CE = FalseSym0
TFHelper_0123456789876543210 CY CF = FalseSym0
TFHelper_0123456789876543210 CY CG = FalseSym0
TFHelper_0123456789876543210 CY CH = FalseSym0
TFHelper_0123456789876543210 CY CI = FalseSym0
TFHelper_0123456789876543210 CY CJ = FalseSym0
TFHelper_0123456789876543210 CY CK = FalseSym0
TFHelper_0123456789876543210 CY CL = FalseSym0
TFHelper_0123456789876543210 CY CM = FalseSym0
TFHelper_0123456789876543210 CY CN = FalseSym0
TFHelper_0123456789876543210 CY CO = FalseSym0
TFHelper_0123456789876543210 CY CP = FalseSym0
TFHelper_0123456789876543210 CY CQ = FalseSym0
TFHelper_0123456789876543210 CY CR = FalseSym0
TFHelper_0123456789876543210 CY CS = FalseSym0
TFHelper_0123456789876543210 CY CT = FalseSym0
TFHelper_0123456789876543210 CY CU = FalseSym0
TFHelper_0123456789876543210 CY CV = FalseSym0
TFHelper_0123456789876543210 CY CW = FalseSym0
TFHelper_0123456789876543210 CY CX = FalseSym0
TFHelper_0123456789876543210 CY CY = TrueSym0
TFHelper_0123456789876543210 CY CZ = FalseSym0
TFHelper_0123456789876543210 CZ CA = FalseSym0
TFHelper_0123456789876543210 CZ CB = FalseSym0
TFHelper_0123456789876543210 CZ CC = FalseSym0
TFHelper_0123456789876543210 CZ CD = FalseSym0
TFHelper_0123456789876543210 CZ CE = FalseSym0
TFHelper_0123456789876543210 CZ CF = FalseSym0
TFHelper_0123456789876543210 CZ CG = FalseSym0
TFHelper_0123456789876543210 CZ CH = FalseSym0
TFHelper_0123456789876543210 CZ CI = FalseSym0
TFHelper_0123456789876543210 CZ CJ = FalseSym0
TFHelper_0123456789876543210 CZ CK = FalseSym0
TFHelper_0123456789876543210 CZ CL = FalseSym0
TFHelper_0123456789876543210 CZ CM = FalseSym0
TFHelper_0123456789876543210 CZ CN = FalseSym0
TFHelper_0123456789876543210 CZ CO = FalseSym0
TFHelper_0123456789876543210 CZ CP = FalseSym0
TFHelper_0123456789876543210 CZ CQ = FalseSym0
TFHelper_0123456789876543210 CZ CR = FalseSym0
TFHelper_0123456789876543210 CZ CS = FalseSym0
TFHelper_0123456789876543210 CZ CT = FalseSym0
TFHelper_0123456789876543210 CZ CU = FalseSym0
TFHelper_0123456789876543210 CZ CV = FalseSym0
TFHelper_0123456789876543210 CZ CW = FalseSym0
TFHelper_0123456789876543210 CZ CX = FalseSym0
TFHelper_0123456789876543210 CZ CY = FalseSym0
TFHelper_0123456789876543210 CZ CZ = TrueSym0
type TFHelper_0123456789876543210Sym0 :: (~>) AChar ((~>) AChar Bool)
data TFHelper_0123456789876543210Sym0 :: (~>) AChar ((~>) AChar Bool)
where
TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) =>
TFHelper_0123456789876543210Sym0 a0123456789876543210
type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym0KindInference ())
type TFHelper_0123456789876543210Sym1 :: AChar -> (~>) AChar Bool
data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: AChar) :: (~>) AChar Bool
where
TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) =>
TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym1KindInference ())
type TFHelper_0123456789876543210Sym2 :: AChar -> AChar -> Bool
type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: AChar) (a0123456789876543210 :: AChar) :: Bool where
TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance PEq AChar where
type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
sLookup ::
(forall (t :: [AChar]) (t :: Schema).
Sing t
-> Sing t -> Sing (Apply (Apply LookupSym0 t) t :: U) :: Type)
sOccurs ::
(forall (t :: [AChar]) (t :: Schema).
Sing t
-> Sing t -> Sing (Apply (Apply OccursSym0 t) t :: Bool) :: Type)
sDisjoint ::
(forall (t :: Schema) (t :: Schema).
Sing t
-> Sing t -> Sing (Apply (Apply DisjointSym0 t) t :: Bool) :: Type)
sAttrNotIn ::
(forall (t :: Attribute) (t :: Schema).
Sing t
-> Sing t
-> Sing (Apply (Apply AttrNotInSym0 t) t :: Bool) :: Type)
sAppend ::
(forall (t :: Schema) (t :: Schema).
Sing t
-> Sing t -> Sing (Apply (Apply AppendSym0 t) t :: Schema) :: Type)
sLookup _ (SSch SNil) = sUndefined
sLookup
(sName :: Sing name)
(SSch (SCons (SAttr (sName' :: Sing name') (sU :: Sing u))
(sAttrs :: Sing attrs)))
= let
sScrutinee_0123456789876543210 ::
Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs)
sScrutinee_0123456789876543210
= applySing (applySing (singFun2 @(==@#@$) (%==)) sName) sName'
in
GHC.Internal.Base.id
@(Sing (Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs)))
(case sScrutinee_0123456789876543210 of
STrue -> sU
SFalse
-> applySing
(applySing (singFun2 @LookupSym0 sLookup) sName)
(applySing (singFun1 @SchSym0 SSch) sAttrs))
sOccurs _ (SSch SNil) = SFalse
sOccurs
(sName :: Sing name)
(SSch (SCons (SAttr (sName' :: Sing name') _)
(sAttrs :: Sing attrs)))
= applySing
(applySing
(singFun2 @(||@#@$) (%||))
(applySing (applySing (singFun2 @(==@#@$) (%==)) sName) sName'))
(applySing
(applySing (singFun2 @OccursSym0 sOccurs) sName)
(applySing (singFun1 @SchSym0 SSch) sAttrs))
sDisjoint (SSch SNil) _ = STrue
sDisjoint
(SSch (SCons (sH :: Sing h) (sT :: Sing t)))
(sS :: Sing s)
= applySing
(applySing
(singFun2 @(&&@#@$) (%&&))
(applySing (applySing (singFun2 @AttrNotInSym0 sAttrNotIn) sH) sS))
(applySing
(applySing
(singFun2 @DisjointSym0 sDisjoint)
(applySing (singFun1 @SchSym0 SSch) sT))
sS)
sAttrNotIn _ (SSch SNil) = STrue
sAttrNotIn
(SAttr (sName :: Sing name) (sU :: Sing u))
(SSch (SCons (SAttr (sName' :: Sing name') _) (sT :: Sing t)))
= applySing
(applySing
(singFun2 @(&&@#@$) (%&&))
(applySing (applySing (singFun2 @(/=@#@$) (%/=)) sName) sName'))
(applySing
(applySing
(singFun2 @AttrNotInSym0 sAttrNotIn)
(applySing (applySing (singFun2 @AttrSym0 SAttr) sName) sU))
(applySing (singFun1 @SchSym0 SSch) sT))
sAppend (SSch (sS1 :: Sing s1)) (SSch (sS2 :: Sing s2))
= applySing
(singFun1 @SchSym0 SSch)
(applySing (applySing (singFun2 @(++@#@$) (%++)) sS1) sS2)
instance SingI (LookupSym0 :: (~>) [AChar] ((~>) Schema U)) where
sing = singFun2 @LookupSym0 sLookup
instance SingI d =>
SingI (LookupSym1 (d :: [AChar]) :: (~>) Schema U) where
sing = singFun1 @(LookupSym1 (d :: [AChar])) (sLookup (sing @d))
instance SingI1 (LookupSym1 :: [AChar] -> (~>) Schema U) where
liftSing (s :: Sing (d :: [AChar]))
= singFun1 @(LookupSym1 (d :: [AChar])) (sLookup s)
instance SingI (OccursSym0 :: (~>) [AChar] ((~>) Schema Bool)) where
sing = singFun2 @OccursSym0 sOccurs
instance SingI d =>
SingI (OccursSym1 (d :: [AChar]) :: (~>) Schema Bool) where
sing = singFun1 @(OccursSym1 (d :: [AChar])) (sOccurs (sing @d))
instance SingI1 (OccursSym1 :: [AChar] -> (~>) Schema Bool) where
liftSing (s :: Sing (d :: [AChar]))
= singFun1 @(OccursSym1 (d :: [AChar])) (sOccurs s)
instance SingI (DisjointSym0 :: (~>) Schema ((~>) Schema Bool)) where
sing = singFun2 @DisjointSym0 sDisjoint
instance SingI d =>
SingI (DisjointSym1 (d :: Schema) :: (~>) Schema Bool) where
sing = singFun1 @(DisjointSym1 (d :: Schema)) (sDisjoint (sing @d))
instance SingI1 (DisjointSym1 :: Schema -> (~>) Schema Bool) where
liftSing (s :: Sing (d :: Schema))
= singFun1 @(DisjointSym1 (d :: Schema)) (sDisjoint s)
instance SingI (AttrNotInSym0 :: (~>) Attribute ((~>) Schema Bool)) where
sing = singFun2 @AttrNotInSym0 sAttrNotIn
instance SingI d =>
SingI (AttrNotInSym1 (d :: Attribute) :: (~>) Schema Bool) where
sing
= singFun1 @(AttrNotInSym1 (d :: Attribute)) (sAttrNotIn (sing @d))
instance SingI1 (AttrNotInSym1 :: Attribute
-> (~>) Schema Bool) where
liftSing (s :: Sing (d :: Attribute))
= singFun1 @(AttrNotInSym1 (d :: Attribute)) (sAttrNotIn s)
instance SingI (AppendSym0 :: (~>) Schema ((~>) Schema Schema)) where
sing = singFun2 @AppendSym0 sAppend
instance SingI d =>
SingI (AppendSym1 (d :: Schema) :: (~>) Schema Schema) where
sing = singFun1 @(AppendSym1 (d :: Schema)) (sAppend (sing @d))
instance SingI1 (AppendSym1 :: Schema -> (~>) Schema Schema) where
liftSing (s :: Sing (d :: Schema))
= singFun1 @(AppendSym1 (d :: Schema)) (sAppend s)
data SU :: U -> Type
where
SBOOL :: SU (BOOL :: U)
SSTRING :: SU (STRING :: U)
SNAT :: SU (NAT :: U)
SVEC :: forall (n :: U) (n :: Nat).
(Sing n) -> (Sing n) -> SU (VEC n n :: U)
type instance Sing @U = SU
instance SingKind U where
type Demote U = U
fromSing SBOOL = BOOL
fromSing SSTRING = STRING
fromSing SNAT = NAT
fromSing (SVEC b b) = VEC (fromSing b) (fromSing b)
toSing BOOL = SomeSing SBOOL
toSing STRING = SomeSing SSTRING
toSing NAT = SomeSing SNAT
toSing (VEC (b :: Demote U) (b :: Demote Nat))
= case (,) (toSing b :: SomeSing U) (toSing b :: SomeSing Nat) of
(,) (SomeSing c) (SomeSing c) -> SomeSing (SVEC c c)
data SAChar :: AChar -> Type
where
SCA :: SAChar (CA :: AChar)
SCB :: SAChar (CB :: AChar)
SCC :: SAChar (CC :: AChar)
SCD :: SAChar (CD :: AChar)
SCE :: SAChar (CE :: AChar)
SCF :: SAChar (CF :: AChar)
SCG :: SAChar (CG :: AChar)
SCH :: SAChar (CH :: AChar)
SCI :: SAChar (CI :: AChar)
SCJ :: SAChar (CJ :: AChar)
SCK :: SAChar (CK :: AChar)
SCL :: SAChar (CL :: AChar)
SCM :: SAChar (CM :: AChar)
SCN :: SAChar (CN :: AChar)
SCO :: SAChar (CO :: AChar)
SCP :: SAChar (CP :: AChar)
SCQ :: SAChar (CQ :: AChar)
SCR :: SAChar (CR :: AChar)
SCS :: SAChar (CS :: AChar)
SCT :: SAChar (CT :: AChar)
SCU :: SAChar (CU :: AChar)
SCV :: SAChar (CV :: AChar)
SCW :: SAChar (CW :: AChar)
SCX :: SAChar (CX :: AChar)
SCY :: SAChar (CY :: AChar)
SCZ :: SAChar (CZ :: AChar)
type instance Sing @AChar = SAChar
instance SingKind AChar where
type Demote AChar = AChar
fromSing SCA = CA
fromSing SCB = CB
fromSing SCC = CC
fromSing SCD = CD
fromSing SCE = CE
fromSing SCF = CF
fromSing SCG = CG
fromSing SCH = CH
fromSing SCI = CI
fromSing SCJ = CJ
fromSing SCK = CK
fromSing SCL = CL
fromSing SCM = CM
fromSing SCN = CN
fromSing SCO = CO
fromSing SCP = CP
fromSing SCQ = CQ
fromSing SCR = CR
fromSing SCS = CS
fromSing SCT = CT
fromSing SCU = CU
fromSing SCV = CV
fromSing SCW = CW
fromSing SCX = CX
fromSing SCY = CY
fromSing SCZ = CZ
toSing CA = SomeSing SCA
toSing CB = SomeSing SCB
toSing CC = SomeSing SCC
toSing CD = SomeSing SCD
toSing CE = SomeSing SCE
toSing CF = SomeSing SCF
toSing CG = SomeSing SCG
toSing CH = SomeSing SCH
toSing CI = SomeSing SCI
toSing CJ = SomeSing SCJ
toSing CK = SomeSing SCK
toSing CL = SomeSing SCL
toSing CM = SomeSing SCM
toSing CN = SomeSing SCN
toSing CO = SomeSing SCO
toSing CP = SomeSing SCP
toSing CQ = SomeSing SCQ
toSing CR = SomeSing SCR
toSing CS = SomeSing SCS
toSing CT = SomeSing SCT
toSing CU = SomeSing SCU
toSing CV = SomeSing SCV
toSing CW = SomeSing SCW
toSing CX = SomeSing SCX
toSing CY = SomeSing SCY
toSing CZ = SomeSing SCZ
data SAttribute :: Attribute -> Type
where
SAttr :: forall (n :: [AChar]) (n :: U).
(Sing n) -> (Sing n) -> SAttribute (Attr n n :: Attribute)
type instance Sing @Attribute = SAttribute
instance SingKind Attribute where
type Demote Attribute = Attribute
fromSing (SAttr b b) = Attr (fromSing b) (fromSing b)
toSing (Attr (b :: Demote [AChar]) (b :: Demote U))
= case
(,) (toSing b :: SomeSing [AChar]) (toSing b :: SomeSing U)
of
(,) (SomeSing c) (SomeSing c) -> SomeSing (SAttr c c)
data SSchema :: Schema -> Type
where
SSch :: forall (n :: [Attribute]).
(Sing n) -> SSchema (Sch n :: Schema)
type instance Sing @Schema = SSchema
instance SingKind Schema where
type Demote Schema = Schema
fromSing (SSch b) = Sch (fromSing b)
toSing (Sch (b :: Demote [Attribute]))
= case toSing b :: SomeSing [Attribute] of
SomeSing c -> SomeSing (SSch c)
instance (SEq U, SEq Nat) => SEq U where
(%==) ::
forall (t1 :: U) (t2 :: U). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun U ((~>) U Bool)
-> Type) t1) t2)
(%==) SBOOL SBOOL = STrue
(%==) SBOOL SSTRING = SFalse
(%==) SBOOL SNAT = SFalse
(%==) SBOOL (SVEC _ _) = SFalse
(%==) SSTRING SBOOL = SFalse
(%==) SSTRING SSTRING = STrue
(%==) SSTRING SNAT = SFalse
(%==) SSTRING (SVEC _ _) = SFalse
(%==) SNAT SBOOL = SFalse
(%==) SNAT SSTRING = SFalse
(%==) SNAT SNAT = STrue
(%==) SNAT (SVEC _ _) = SFalse
(%==) (SVEC _ _) SBOOL = SFalse
(%==) (SVEC _ _) SSTRING = SFalse
(%==) (SVEC _ _) SNAT = SFalse
(%==)
(SVEC (sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210))
(SVEC (sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing
(singFun2 @(&&@#@$) (%&&))
(applySing
(applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
sB_0123456789876543210)
instance (SShow U, SShow Nat) => SShow U where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: U)
(t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) U ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
SBOOL
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "BOOL"))
sA_0123456789876543210
sShowsPrec
_
SSTRING
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "STRING"))
sA_0123456789876543210
sShowsPrec
_
SNAT
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "NAT"))
sA_0123456789876543210
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
(SVEC (sArg_0123456789876543210 :: Sing arg_0123456789876543210)
(sArg_0123456789876543210 :: Sing arg_0123456789876543210))
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(applySing
(singFun3 @ShowParenSym0 sShowParen)
(applySing
(applySing (singFun2 @(>@#@$) (%>)) sP_0123456789876543210)
(sFromInteger (sing :: Sing 10))))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "VEC ")))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 11)))
sArg_0123456789876543210))
(applySing
(applySing
(singFun3 @(.@#@$) (%.)) (singFun1 @ShowSpaceSym0 sShowSpace))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 11)))
sArg_0123456789876543210)))))
sA_0123456789876543210
instance SShow AChar where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: AChar)
(t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) AChar ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
SCA
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CA"))
sA_0123456789876543210
sShowsPrec
_
SCB
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CB"))
sA_0123456789876543210
sShowsPrec
_
SCC
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CC"))
sA_0123456789876543210
sShowsPrec
_
SCD
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CD"))
sA_0123456789876543210
sShowsPrec
_
SCE
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CE"))
sA_0123456789876543210
sShowsPrec
_
SCF
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CF"))
sA_0123456789876543210
sShowsPrec
_
SCG
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CG"))
sA_0123456789876543210
sShowsPrec
_
SCH
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CH"))
sA_0123456789876543210
sShowsPrec
_
SCI
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CI"))
sA_0123456789876543210
sShowsPrec
_
SCJ
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CJ"))
sA_0123456789876543210
sShowsPrec
_
SCK
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CK"))
sA_0123456789876543210
sShowsPrec
_
SCL
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CL"))
sA_0123456789876543210
sShowsPrec
_
SCM
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CM"))
sA_0123456789876543210
sShowsPrec
_
SCN
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CN"))
sA_0123456789876543210
sShowsPrec
_
SCO
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CO"))
sA_0123456789876543210
sShowsPrec
_
SCP
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CP"))
sA_0123456789876543210
sShowsPrec
_
SCQ
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CQ"))
sA_0123456789876543210
sShowsPrec
_
SCR
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CR"))
sA_0123456789876543210
sShowsPrec
_
SCS
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CS"))
sA_0123456789876543210
sShowsPrec
_
SCT
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CT"))
sA_0123456789876543210
sShowsPrec
_
SCU
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CU"))
sA_0123456789876543210
sShowsPrec
_
SCV
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CV"))
sA_0123456789876543210
sShowsPrec
_
SCW
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CW"))
sA_0123456789876543210
sShowsPrec
_
SCX
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CX"))
sA_0123456789876543210
sShowsPrec
_
SCY
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CY"))
sA_0123456789876543210
sShowsPrec
_
SCZ
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CZ"))
sA_0123456789876543210
instance SEq AChar where
(%==) ::
forall (t1 :: AChar) (t2 :: AChar). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun AChar ((~>) AChar Bool)
-> Type) t1) t2)
(%==) SCA SCA = STrue
(%==) SCA SCB = SFalse
(%==) SCA SCC = SFalse
(%==) SCA SCD = SFalse
(%==) SCA SCE = SFalse
(%==) SCA SCF = SFalse
(%==) SCA SCG = SFalse
(%==) SCA SCH = SFalse
(%==) SCA SCI = SFalse
(%==) SCA SCJ = SFalse
(%==) SCA SCK = SFalse
(%==) SCA SCL = SFalse
(%==) SCA SCM = SFalse
(%==) SCA SCN = SFalse
(%==) SCA SCO = SFalse
(%==) SCA SCP = SFalse
(%==) SCA SCQ = SFalse
(%==) SCA SCR = SFalse
(%==) SCA SCS = SFalse
(%==) SCA SCT = SFalse
(%==) SCA SCU = SFalse
(%==) SCA SCV = SFalse
(%==) SCA SCW = SFalse
(%==) SCA SCX = SFalse
(%==) SCA SCY = SFalse
(%==) SCA SCZ = SFalse
(%==) SCB SCA = SFalse
(%==) SCB SCB = STrue
(%==) SCB SCC = SFalse
(%==) SCB SCD = SFalse
(%==) SCB SCE = SFalse
(%==) SCB SCF = SFalse
(%==) SCB SCG = SFalse
(%==) SCB SCH = SFalse
(%==) SCB SCI = SFalse
(%==) SCB SCJ = SFalse
(%==) SCB SCK = SFalse
(%==) SCB SCL = SFalse
(%==) SCB SCM = SFalse
(%==) SCB SCN = SFalse
(%==) SCB SCO = SFalse
(%==) SCB SCP = SFalse
(%==) SCB SCQ = SFalse
(%==) SCB SCR = SFalse
(%==) SCB SCS = SFalse
(%==) SCB SCT = SFalse
(%==) SCB SCU = SFalse
(%==) SCB SCV = SFalse
(%==) SCB SCW = SFalse
(%==) SCB SCX = SFalse
(%==) SCB SCY = SFalse
(%==) SCB SCZ = SFalse
(%==) SCC SCA = SFalse
(%==) SCC SCB = SFalse
(%==) SCC SCC = STrue
(%==) SCC SCD = SFalse
(%==) SCC SCE = SFalse
(%==) SCC SCF = SFalse
(%==) SCC SCG = SFalse
(%==) SCC SCH = SFalse
(%==) SCC SCI = SFalse
(%==) SCC SCJ = SFalse
(%==) SCC SCK = SFalse
(%==) SCC SCL = SFalse
(%==) SCC SCM = SFalse
(%==) SCC SCN = SFalse
(%==) SCC SCO = SFalse
(%==) SCC SCP = SFalse
(%==) SCC SCQ = SFalse
(%==) SCC SCR = SFalse
(%==) SCC SCS = SFalse
(%==) SCC SCT = SFalse
(%==) SCC SCU = SFalse
(%==) SCC SCV = SFalse
(%==) SCC SCW = SFalse
(%==) SCC SCX = SFalse
(%==) SCC SCY = SFalse
(%==) SCC SCZ = SFalse
(%==) SCD SCA = SFalse
(%==) SCD SCB = SFalse
(%==) SCD SCC = SFalse
(%==) SCD SCD = STrue
(%==) SCD SCE = SFalse
(%==) SCD SCF = SFalse
(%==) SCD SCG = SFalse
(%==) SCD SCH = SFalse
(%==) SCD SCI = SFalse
(%==) SCD SCJ = SFalse
(%==) SCD SCK = SFalse
(%==) SCD SCL = SFalse
(%==) SCD SCM = SFalse
(%==) SCD SCN = SFalse
(%==) SCD SCO = SFalse
(%==) SCD SCP = SFalse
(%==) SCD SCQ = SFalse
(%==) SCD SCR = SFalse
(%==) SCD SCS = SFalse
(%==) SCD SCT = SFalse
(%==) SCD SCU = SFalse
(%==) SCD SCV = SFalse
(%==) SCD SCW = SFalse
(%==) SCD SCX = SFalse
(%==) SCD SCY = SFalse
(%==) SCD SCZ = SFalse
(%==) SCE SCA = SFalse
(%==) SCE SCB = SFalse
(%==) SCE SCC = SFalse
(%==) SCE SCD = SFalse
(%==) SCE SCE = STrue
(%==) SCE SCF = SFalse
(%==) SCE SCG = SFalse
(%==) SCE SCH = SFalse
(%==) SCE SCI = SFalse
(%==) SCE SCJ = SFalse
(%==) SCE SCK = SFalse
(%==) SCE SCL = SFalse
(%==) SCE SCM = SFalse
(%==) SCE SCN = SFalse
(%==) SCE SCO = SFalse
(%==) SCE SCP = SFalse
(%==) SCE SCQ = SFalse
(%==) SCE SCR = SFalse
(%==) SCE SCS = SFalse
(%==) SCE SCT = SFalse
(%==) SCE SCU = SFalse
(%==) SCE SCV = SFalse
(%==) SCE SCW = SFalse
(%==) SCE SCX = SFalse
(%==) SCE SCY = SFalse
(%==) SCE SCZ = SFalse
(%==) SCF SCA = SFalse
(%==) SCF SCB = SFalse
(%==) SCF SCC = SFalse
(%==) SCF SCD = SFalse
(%==) SCF SCE = SFalse
(%==) SCF SCF = STrue
(%==) SCF SCG = SFalse
(%==) SCF SCH = SFalse
(%==) SCF SCI = SFalse
(%==) SCF SCJ = SFalse
(%==) SCF SCK = SFalse
(%==) SCF SCL = SFalse
(%==) SCF SCM = SFalse
(%==) SCF SCN = SFalse
(%==) SCF SCO = SFalse
(%==) SCF SCP = SFalse
(%==) SCF SCQ = SFalse
(%==) SCF SCR = SFalse
(%==) SCF SCS = SFalse
(%==) SCF SCT = SFalse
(%==) SCF SCU = SFalse
(%==) SCF SCV = SFalse
(%==) SCF SCW = SFalse
(%==) SCF SCX = SFalse
(%==) SCF SCY = SFalse
(%==) SCF SCZ = SFalse
(%==) SCG SCA = SFalse
(%==) SCG SCB = SFalse
(%==) SCG SCC = SFalse
(%==) SCG SCD = SFalse
(%==) SCG SCE = SFalse
(%==) SCG SCF = SFalse
(%==) SCG SCG = STrue
(%==) SCG SCH = SFalse
(%==) SCG SCI = SFalse
(%==) SCG SCJ = SFalse
(%==) SCG SCK = SFalse
(%==) SCG SCL = SFalse
(%==) SCG SCM = SFalse
(%==) SCG SCN = SFalse
(%==) SCG SCO = SFalse
(%==) SCG SCP = SFalse
(%==) SCG SCQ = SFalse
(%==) SCG SCR = SFalse
(%==) SCG SCS = SFalse
(%==) SCG SCT = SFalse
(%==) SCG SCU = SFalse
(%==) SCG SCV = SFalse
(%==) SCG SCW = SFalse
(%==) SCG SCX = SFalse
(%==) SCG SCY = SFalse
(%==) SCG SCZ = SFalse
(%==) SCH SCA = SFalse
(%==) SCH SCB = SFalse
(%==) SCH SCC = SFalse
(%==) SCH SCD = SFalse
(%==) SCH SCE = SFalse
(%==) SCH SCF = SFalse
(%==) SCH SCG = SFalse
(%==) SCH SCH = STrue
(%==) SCH SCI = SFalse
(%==) SCH SCJ = SFalse
(%==) SCH SCK = SFalse
(%==) SCH SCL = SFalse
(%==) SCH SCM = SFalse
(%==) SCH SCN = SFalse
(%==) SCH SCO = SFalse
(%==) SCH SCP = SFalse
(%==) SCH SCQ = SFalse
(%==) SCH SCR = SFalse
(%==) SCH SCS = SFalse
(%==) SCH SCT = SFalse
(%==) SCH SCU = SFalse
(%==) SCH SCV = SFalse
(%==) SCH SCW = SFalse
(%==) SCH SCX = SFalse
(%==) SCH SCY = SFalse
(%==) SCH SCZ = SFalse
(%==) SCI SCA = SFalse
(%==) SCI SCB = SFalse
(%==) SCI SCC = SFalse
(%==) SCI SCD = SFalse
(%==) SCI SCE = SFalse
(%==) SCI SCF = SFalse
(%==) SCI SCG = SFalse
(%==) SCI SCH = SFalse
(%==) SCI SCI = STrue
(%==) SCI SCJ = SFalse
(%==) SCI SCK = SFalse
(%==) SCI SCL = SFalse
(%==) SCI SCM = SFalse
(%==) SCI SCN = SFalse
(%==) SCI SCO = SFalse
(%==) SCI SCP = SFalse
(%==) SCI SCQ = SFalse
(%==) SCI SCR = SFalse
(%==) SCI SCS = SFalse
(%==) SCI SCT = SFalse
(%==) SCI SCU = SFalse
(%==) SCI SCV = SFalse
(%==) SCI SCW = SFalse
(%==) SCI SCX = SFalse
(%==) SCI SCY = SFalse
(%==) SCI SCZ = SFalse
(%==) SCJ SCA = SFalse
(%==) SCJ SCB = SFalse
(%==) SCJ SCC = SFalse
(%==) SCJ SCD = SFalse
(%==) SCJ SCE = SFalse
(%==) SCJ SCF = SFalse
(%==) SCJ SCG = SFalse
(%==) SCJ SCH = SFalse
(%==) SCJ SCI = SFalse
(%==) SCJ SCJ = STrue
(%==) SCJ SCK = SFalse
(%==) SCJ SCL = SFalse
(%==) SCJ SCM = SFalse
(%==) SCJ SCN = SFalse
(%==) SCJ SCO = SFalse
(%==) SCJ SCP = SFalse
(%==) SCJ SCQ = SFalse
(%==) SCJ SCR = SFalse
(%==) SCJ SCS = SFalse
(%==) SCJ SCT = SFalse
(%==) SCJ SCU = SFalse
(%==) SCJ SCV = SFalse
(%==) SCJ SCW = SFalse
(%==) SCJ SCX = SFalse
(%==) SCJ SCY = SFalse
(%==) SCJ SCZ = SFalse
(%==) SCK SCA = SFalse
(%==) SCK SCB = SFalse
(%==) SCK SCC = SFalse
(%==) SCK SCD = SFalse
(%==) SCK SCE = SFalse
(%==) SCK SCF = SFalse
(%==) SCK SCG = SFalse
(%==) SCK SCH = SFalse
(%==) SCK SCI = SFalse
(%==) SCK SCJ = SFalse
(%==) SCK SCK = STrue
(%==) SCK SCL = SFalse
(%==) SCK SCM = SFalse
(%==) SCK SCN = SFalse
(%==) SCK SCO = SFalse
(%==) SCK SCP = SFalse
(%==) SCK SCQ = SFalse
(%==) SCK SCR = SFalse
(%==) SCK SCS = SFalse
(%==) SCK SCT = SFalse
(%==) SCK SCU = SFalse
(%==) SCK SCV = SFalse
(%==) SCK SCW = SFalse
(%==) SCK SCX = SFalse
(%==) SCK SCY = SFalse
(%==) SCK SCZ = SFalse
(%==) SCL SCA = SFalse
(%==) SCL SCB = SFalse
(%==) SCL SCC = SFalse
(%==) SCL SCD = SFalse
(%==) SCL SCE = SFalse
(%==) SCL SCF = SFalse
(%==) SCL SCG = SFalse
(%==) SCL SCH = SFalse
(%==) SCL SCI = SFalse
(%==) SCL SCJ = SFalse
(%==) SCL SCK = SFalse
(%==) SCL SCL = STrue
(%==) SCL SCM = SFalse
(%==) SCL SCN = SFalse
(%==) SCL SCO = SFalse
(%==) SCL SCP = SFalse
(%==) SCL SCQ = SFalse
(%==) SCL SCR = SFalse
(%==) SCL SCS = SFalse
(%==) SCL SCT = SFalse
(%==) SCL SCU = SFalse
(%==) SCL SCV = SFalse
(%==) SCL SCW = SFalse
(%==) SCL SCX = SFalse
(%==) SCL SCY = SFalse
(%==) SCL SCZ = SFalse
(%==) SCM SCA = SFalse
(%==) SCM SCB = SFalse
(%==) SCM SCC = SFalse
(%==) SCM SCD = SFalse
(%==) SCM SCE = SFalse
(%==) SCM SCF = SFalse
(%==) SCM SCG = SFalse
(%==) SCM SCH = SFalse
(%==) SCM SCI = SFalse
(%==) SCM SCJ = SFalse
(%==) SCM SCK = SFalse
(%==) SCM SCL = SFalse
(%==) SCM SCM = STrue
(%==) SCM SCN = SFalse
(%==) SCM SCO = SFalse
(%==) SCM SCP = SFalse
(%==) SCM SCQ = SFalse
(%==) SCM SCR = SFalse
(%==) SCM SCS = SFalse
(%==) SCM SCT = SFalse
(%==) SCM SCU = SFalse
(%==) SCM SCV = SFalse
(%==) SCM SCW = SFalse
(%==) SCM SCX = SFalse
(%==) SCM SCY = SFalse
(%==) SCM SCZ = SFalse
(%==) SCN SCA = SFalse
(%==) SCN SCB = SFalse
(%==) SCN SCC = SFalse
(%==) SCN SCD = SFalse
(%==) SCN SCE = SFalse
(%==) SCN SCF = SFalse
(%==) SCN SCG = SFalse
(%==) SCN SCH = SFalse
(%==) SCN SCI = SFalse
(%==) SCN SCJ = SFalse
(%==) SCN SCK = SFalse
(%==) SCN SCL = SFalse
(%==) SCN SCM = SFalse
(%==) SCN SCN = STrue
(%==) SCN SCO = SFalse
(%==) SCN SCP = SFalse
(%==) SCN SCQ = SFalse
(%==) SCN SCR = SFalse
(%==) SCN SCS = SFalse
(%==) SCN SCT = SFalse
(%==) SCN SCU = SFalse
(%==) SCN SCV = SFalse
(%==) SCN SCW = SFalse
(%==) SCN SCX = SFalse
(%==) SCN SCY = SFalse
(%==) SCN SCZ = SFalse
(%==) SCO SCA = SFalse
(%==) SCO SCB = SFalse
(%==) SCO SCC = SFalse
(%==) SCO SCD = SFalse
(%==) SCO SCE = SFalse
(%==) SCO SCF = SFalse
(%==) SCO SCG = SFalse
(%==) SCO SCH = SFalse
(%==) SCO SCI = SFalse
(%==) SCO SCJ = SFalse
(%==) SCO SCK = SFalse
(%==) SCO SCL = SFalse
(%==) SCO SCM = SFalse
(%==) SCO SCN = SFalse
(%==) SCO SCO = STrue
(%==) SCO SCP = SFalse
(%==) SCO SCQ = SFalse
(%==) SCO SCR = SFalse
(%==) SCO SCS = SFalse
(%==) SCO SCT = SFalse
(%==) SCO SCU = SFalse
(%==) SCO SCV = SFalse
(%==) SCO SCW = SFalse
(%==) SCO SCX = SFalse
(%==) SCO SCY = SFalse
(%==) SCO SCZ = SFalse
(%==) SCP SCA = SFalse
(%==) SCP SCB = SFalse
(%==) SCP SCC = SFalse
(%==) SCP SCD = SFalse
(%==) SCP SCE = SFalse
(%==) SCP SCF = SFalse
(%==) SCP SCG = SFalse
(%==) SCP SCH = SFalse
(%==) SCP SCI = SFalse
(%==) SCP SCJ = SFalse
(%==) SCP SCK = SFalse
(%==) SCP SCL = SFalse
(%==) SCP SCM = SFalse
(%==) SCP SCN = SFalse
(%==) SCP SCO = SFalse
(%==) SCP SCP = STrue
(%==) SCP SCQ = SFalse
(%==) SCP SCR = SFalse
(%==) SCP SCS = SFalse
(%==) SCP SCT = SFalse
(%==) SCP SCU = SFalse
(%==) SCP SCV = SFalse
(%==) SCP SCW = SFalse
(%==) SCP SCX = SFalse
(%==) SCP SCY = SFalse
(%==) SCP SCZ = SFalse
(%==) SCQ SCA = SFalse
(%==) SCQ SCB = SFalse
(%==) SCQ SCC = SFalse
(%==) SCQ SCD = SFalse
(%==) SCQ SCE = SFalse
(%==) SCQ SCF = SFalse
(%==) SCQ SCG = SFalse
(%==) SCQ SCH = SFalse
(%==) SCQ SCI = SFalse
(%==) SCQ SCJ = SFalse
(%==) SCQ SCK = SFalse
(%==) SCQ SCL = SFalse
(%==) SCQ SCM = SFalse
(%==) SCQ SCN = SFalse
(%==) SCQ SCO = SFalse
(%==) SCQ SCP = SFalse
(%==) SCQ SCQ = STrue
(%==) SCQ SCR = SFalse
(%==) SCQ SCS = SFalse
(%==) SCQ SCT = SFalse
(%==) SCQ SCU = SFalse
(%==) SCQ SCV = SFalse
(%==) SCQ SCW = SFalse
(%==) SCQ SCX = SFalse
(%==) SCQ SCY = SFalse
(%==) SCQ SCZ = SFalse
(%==) SCR SCA = SFalse
(%==) SCR SCB = SFalse
(%==) SCR SCC = SFalse
(%==) SCR SCD = SFalse
(%==) SCR SCE = SFalse
(%==) SCR SCF = SFalse
(%==) SCR SCG = SFalse
(%==) SCR SCH = SFalse
(%==) SCR SCI = SFalse
(%==) SCR SCJ = SFalse
(%==) SCR SCK = SFalse
(%==) SCR SCL = SFalse
(%==) SCR SCM = SFalse
(%==) SCR SCN = SFalse
(%==) SCR SCO = SFalse
(%==) SCR SCP = SFalse
(%==) SCR SCQ = SFalse
(%==) SCR SCR = STrue
(%==) SCR SCS = SFalse
(%==) SCR SCT = SFalse
(%==) SCR SCU = SFalse
(%==) SCR SCV = SFalse
(%==) SCR SCW = SFalse
(%==) SCR SCX = SFalse
(%==) SCR SCY = SFalse
(%==) SCR SCZ = SFalse
(%==) SCS SCA = SFalse
(%==) SCS SCB = SFalse
(%==) SCS SCC = SFalse
(%==) SCS SCD = SFalse
(%==) SCS SCE = SFalse
(%==) SCS SCF = SFalse
(%==) SCS SCG = SFalse
(%==) SCS SCH = SFalse
(%==) SCS SCI = SFalse
(%==) SCS SCJ = SFalse
(%==) SCS SCK = SFalse
(%==) SCS SCL = SFalse
(%==) SCS SCM = SFalse
(%==) SCS SCN = SFalse
(%==) SCS SCO = SFalse
(%==) SCS SCP = SFalse
(%==) SCS SCQ = SFalse
(%==) SCS SCR = SFalse
(%==) SCS SCS = STrue
(%==) SCS SCT = SFalse
(%==) SCS SCU = SFalse
(%==) SCS SCV = SFalse
(%==) SCS SCW = SFalse
(%==) SCS SCX = SFalse
(%==) SCS SCY = SFalse
(%==) SCS SCZ = SFalse
(%==) SCT SCA = SFalse
(%==) SCT SCB = SFalse
(%==) SCT SCC = SFalse
(%==) SCT SCD = SFalse
(%==) SCT SCE = SFalse
(%==) SCT SCF = SFalse
(%==) SCT SCG = SFalse
(%==) SCT SCH = SFalse
(%==) SCT SCI = SFalse
(%==) SCT SCJ = SFalse
(%==) SCT SCK = SFalse
(%==) SCT SCL = SFalse
(%==) SCT SCM = SFalse
(%==) SCT SCN = SFalse
(%==) SCT SCO = SFalse
(%==) SCT SCP = SFalse
(%==) SCT SCQ = SFalse
(%==) SCT SCR = SFalse
(%==) SCT SCS = SFalse
(%==) SCT SCT = STrue
(%==) SCT SCU = SFalse
(%==) SCT SCV = SFalse
(%==) SCT SCW = SFalse
(%==) SCT SCX = SFalse
(%==) SCT SCY = SFalse
(%==) SCT SCZ = SFalse
(%==) SCU SCA = SFalse
(%==) SCU SCB = SFalse
(%==) SCU SCC = SFalse
(%==) SCU SCD = SFalse
(%==) SCU SCE = SFalse
(%==) SCU SCF = SFalse
(%==) SCU SCG = SFalse
(%==) SCU SCH = SFalse
(%==) SCU SCI = SFalse
(%==) SCU SCJ = SFalse
(%==) SCU SCK = SFalse
(%==) SCU SCL = SFalse
(%==) SCU SCM = SFalse
(%==) SCU SCN = SFalse
(%==) SCU SCO = SFalse
(%==) SCU SCP = SFalse
(%==) SCU SCQ = SFalse
(%==) SCU SCR = SFalse
(%==) SCU SCS = SFalse
(%==) SCU SCT = SFalse
(%==) SCU SCU = STrue
(%==) SCU SCV = SFalse
(%==) SCU SCW = SFalse
(%==) SCU SCX = SFalse
(%==) SCU SCY = SFalse
(%==) SCU SCZ = SFalse
(%==) SCV SCA = SFalse
(%==) SCV SCB = SFalse
(%==) SCV SCC = SFalse
(%==) SCV SCD = SFalse
(%==) SCV SCE = SFalse
(%==) SCV SCF = SFalse
(%==) SCV SCG = SFalse
(%==) SCV SCH = SFalse
(%==) SCV SCI = SFalse
(%==) SCV SCJ = SFalse
(%==) SCV SCK = SFalse
(%==) SCV SCL = SFalse
(%==) SCV SCM = SFalse
(%==) SCV SCN = SFalse
(%==) SCV SCO = SFalse
(%==) SCV SCP = SFalse
(%==) SCV SCQ = SFalse
(%==) SCV SCR = SFalse
(%==) SCV SCS = SFalse
(%==) SCV SCT = SFalse
(%==) SCV SCU = SFalse
(%==) SCV SCV = STrue
(%==) SCV SCW = SFalse
(%==) SCV SCX = SFalse
(%==) SCV SCY = SFalse
(%==) SCV SCZ = SFalse
(%==) SCW SCA = SFalse
(%==) SCW SCB = SFalse
(%==) SCW SCC = SFalse
(%==) SCW SCD = SFalse
(%==) SCW SCE = SFalse
(%==) SCW SCF = SFalse
(%==) SCW SCG = SFalse
(%==) SCW SCH = SFalse
(%==) SCW SCI = SFalse
(%==) SCW SCJ = SFalse
(%==) SCW SCK = SFalse
(%==) SCW SCL = SFalse
(%==) SCW SCM = SFalse
(%==) SCW SCN = SFalse
(%==) SCW SCO = SFalse
(%==) SCW SCP = SFalse
(%==) SCW SCQ = SFalse
(%==) SCW SCR = SFalse
(%==) SCW SCS = SFalse
(%==) SCW SCT = SFalse
(%==) SCW SCU = SFalse
(%==) SCW SCV = SFalse
(%==) SCW SCW = STrue
(%==) SCW SCX = SFalse
(%==) SCW SCY = SFalse
(%==) SCW SCZ = SFalse
(%==) SCX SCA = SFalse
(%==) SCX SCB = SFalse
(%==) SCX SCC = SFalse
(%==) SCX SCD = SFalse
(%==) SCX SCE = SFalse
(%==) SCX SCF = SFalse
(%==) SCX SCG = SFalse
(%==) SCX SCH = SFalse
(%==) SCX SCI = SFalse
(%==) SCX SCJ = SFalse
(%==) SCX SCK = SFalse
(%==) SCX SCL = SFalse
(%==) SCX SCM = SFalse
(%==) SCX SCN = SFalse
(%==) SCX SCO = SFalse
(%==) SCX SCP = SFalse
(%==) SCX SCQ = SFalse
(%==) SCX SCR = SFalse
(%==) SCX SCS = SFalse
(%==) SCX SCT = SFalse
(%==) SCX SCU = SFalse
(%==) SCX SCV = SFalse
(%==) SCX SCW = SFalse
(%==) SCX SCX = STrue
(%==) SCX SCY = SFalse
(%==) SCX SCZ = SFalse
(%==) SCY SCA = SFalse
(%==) SCY SCB = SFalse
(%==) SCY SCC = SFalse
(%==) SCY SCD = SFalse
(%==) SCY SCE = SFalse
(%==) SCY SCF = SFalse
(%==) SCY SCG = SFalse
(%==) SCY SCH = SFalse
(%==) SCY SCI = SFalse
(%==) SCY SCJ = SFalse
(%==) SCY SCK = SFalse
(%==) SCY SCL = SFalse
(%==) SCY SCM = SFalse
(%==) SCY SCN = SFalse
(%==) SCY SCO = SFalse
(%==) SCY SCP = SFalse
(%==) SCY SCQ = SFalse
(%==) SCY SCR = SFalse
(%==) SCY SCS = SFalse
(%==) SCY SCT = SFalse
(%==) SCY SCU = SFalse
(%==) SCY SCV = SFalse
(%==) SCY SCW = SFalse
(%==) SCY SCX = SFalse
(%==) SCY SCY = STrue
(%==) SCY SCZ = SFalse
(%==) SCZ SCA = SFalse
(%==) SCZ SCB = SFalse
(%==) SCZ SCC = SFalse
(%==) SCZ SCD = SFalse
(%==) SCZ SCE = SFalse
(%==) SCZ SCF = SFalse
(%==) SCZ SCG = SFalse
(%==) SCZ SCH = SFalse
(%==) SCZ SCI = SFalse
(%==) SCZ SCJ = SFalse
(%==) SCZ SCK = SFalse
(%==) SCZ SCL = SFalse
(%==) SCZ SCM = SFalse
(%==) SCZ SCN = SFalse
(%==) SCZ SCO = SFalse
(%==) SCZ SCP = SFalse
(%==) SCZ SCQ = SFalse
(%==) SCZ SCR = SFalse
(%==) SCZ SCS = SFalse
(%==) SCZ SCT = SFalse
(%==) SCZ SCU = SFalse
(%==) SCZ SCV = SFalse
(%==) SCZ SCW = SFalse
(%==) SCZ SCX = SFalse
(%==) SCZ SCY = SFalse
(%==) SCZ SCZ = STrue
instance (SDecide U, SDecide Nat) => SDecide U where
(%~) SBOOL SBOOL = Proved Refl
(%~) SBOOL SSTRING = Disproved (\ x -> case x of {})
(%~) SBOOL SNAT = Disproved (\ x -> case x of {})
(%~) SBOOL (SVEC _ _) = Disproved (\ x -> case x of {})
(%~) SSTRING SBOOL = Disproved (\ x -> case x of {})
(%~) SSTRING SSTRING = Proved Refl
(%~) SSTRING SNAT = Disproved (\ x -> case x of {})
(%~) SSTRING (SVEC _ _) = Disproved (\ x -> case x of {})
(%~) SNAT SBOOL = Disproved (\ x -> case x of {})
(%~) SNAT SSTRING = Disproved (\ x -> case x of {})
(%~) SNAT SNAT = Proved Refl
(%~) SNAT (SVEC _ _) = Disproved (\ x -> case x of {})
(%~) (SVEC _ _) SBOOL = Disproved (\ x -> case x of {})
(%~) (SVEC _ _) SSTRING = Disproved (\ x -> case x of {})
(%~) (SVEC _ _) SNAT = Disproved (\ x -> case x of {})
(%~) (SVEC a a) (SVEC b b)
= case (,) ((%~) a b) ((%~) a b) of
(,) (Proved Refl) (Proved Refl) -> Proved Refl
(,) (Disproved contra) _
-> Disproved (\ refl -> case refl of Refl -> contra Refl)
(,) _ (Disproved contra)
-> Disproved (\ refl -> case refl of Refl -> contra Refl)
instance Eq (SU (z :: U)) where
(==) _ _ = True
instance (SDecide U, SDecide Nat) =>
GHC.Internal.Data.Type.Equality.TestEquality (SU :: U
-> Type) where
GHC.Internal.Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance (SDecide U, SDecide Nat) =>
GHC.Internal.Data.Type.Coercion.TestCoercion (SU :: U
-> Type) where
GHC.Internal.Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
instance SDecide AChar where
(%~) SCA SCA = Proved Refl
(%~) SCA SCB = Disproved (\ x -> case x of {})
(%~) SCA SCC = Disproved (\ x -> case x of {})
(%~) SCA SCD = Disproved (\ x -> case x of {})
(%~) SCA SCE = Disproved (\ x -> case x of {})
(%~) SCA SCF = Disproved (\ x -> case x of {})
(%~) SCA SCG = Disproved (\ x -> case x of {})
(%~) SCA SCH = Disproved (\ x -> case x of {})
(%~) SCA SCI = Disproved (\ x -> case x of {})
(%~) SCA SCJ = Disproved (\ x -> case x of {})
(%~) SCA SCK = Disproved (\ x -> case x of {})
(%~) SCA SCL = Disproved (\ x -> case x of {})
(%~) SCA SCM = Disproved (\ x -> case x of {})
(%~) SCA SCN = Disproved (\ x -> case x of {})
(%~) SCA SCO = Disproved (\ x -> case x of {})
(%~) SCA SCP = Disproved (\ x -> case x of {})
(%~) SCA SCQ = Disproved (\ x -> case x of {})
(%~) SCA SCR = Disproved (\ x -> case x of {})
(%~) SCA SCS = Disproved (\ x -> case x of {})
(%~) SCA SCT = Disproved (\ x -> case x of {})
(%~) SCA SCU = Disproved (\ x -> case x of {})
(%~) SCA SCV = Disproved (\ x -> case x of {})
(%~) SCA SCW = Disproved (\ x -> case x of {})
(%~) SCA SCX = Disproved (\ x -> case x of {})
(%~) SCA SCY = Disproved (\ x -> case x of {})
(%~) SCA SCZ = Disproved (\ x -> case x of {})
(%~) SCB SCA = Disproved (\ x -> case x of {})
(%~) SCB SCB = Proved Refl
(%~) SCB SCC = Disproved (\ x -> case x of {})
(%~) SCB SCD = Disproved (\ x -> case x of {})
(%~) SCB SCE = Disproved (\ x -> case x of {})
(%~) SCB SCF = Disproved (\ x -> case x of {})
(%~) SCB SCG = Disproved (\ x -> case x of {})
(%~) SCB SCH = Disproved (\ x -> case x of {})
(%~) SCB SCI = Disproved (\ x -> case x of {})
(%~) SCB SCJ = Disproved (\ x -> case x of {})
(%~) SCB SCK = Disproved (\ x -> case x of {})
(%~) SCB SCL = Disproved (\ x -> case x of {})
(%~) SCB SCM = Disproved (\ x -> case x of {})
(%~) SCB SCN = Disproved (\ x -> case x of {})
(%~) SCB SCO = Disproved (\ x -> case x of {})
(%~) SCB SCP = Disproved (\ x -> case x of {})
(%~) SCB SCQ = Disproved (\ x -> case x of {})
(%~) SCB SCR = Disproved (\ x -> case x of {})
(%~) SCB SCS = Disproved (\ x -> case x of {})
(%~) SCB SCT = Disproved (\ x -> case x of {})
(%~) SCB SCU = Disproved (\ x -> case x of {})
(%~) SCB SCV = Disproved (\ x -> case x of {})
(%~) SCB SCW = Disproved (\ x -> case x of {})
(%~) SCB SCX = Disproved (\ x -> case x of {})
(%~) SCB SCY = Disproved (\ x -> case x of {})
(%~) SCB SCZ = Disproved (\ x -> case x of {})
(%~) SCC SCA = Disproved (\ x -> case x of {})
(%~) SCC SCB = Disproved (\ x -> case x of {})
(%~) SCC SCC = Proved Refl
(%~) SCC SCD = Disproved (\ x -> case x of {})
(%~) SCC SCE = Disproved (\ x -> case x of {})
(%~) SCC SCF = Disproved (\ x -> case x of {})
(%~) SCC SCG = Disproved (\ x -> case x of {})
(%~) SCC SCH = Disproved (\ x -> case x of {})
(%~) SCC SCI = Disproved (\ x -> case x of {})
(%~) SCC SCJ = Disproved (\ x -> case x of {})
(%~) SCC SCK = Disproved (\ x -> case x of {})
(%~) SCC SCL = Disproved (\ x -> case x of {})
(%~) SCC SCM = Disproved (\ x -> case x of {})
(%~) SCC SCN = Disproved (\ x -> case x of {})
(%~) SCC SCO = Disproved (\ x -> case x of {})
(%~) SCC SCP = Disproved (\ x -> case x of {})
(%~) SCC SCQ = Disproved (\ x -> case x of {})
(%~) SCC SCR = Disproved (\ x -> case x of {})
(%~) SCC SCS = Disproved (\ x -> case x of {})
(%~) SCC SCT = Disproved (\ x -> case x of {})
(%~) SCC SCU = Disproved (\ x -> case x of {})
(%~) SCC SCV = Disproved (\ x -> case x of {})
(%~) SCC SCW = Disproved (\ x -> case x of {})
(%~) SCC SCX = Disproved (\ x -> case x of {})
(%~) SCC SCY = Disproved (\ x -> case x of {})
(%~) SCC SCZ = Disproved (\ x -> case x of {})
(%~) SCD SCA = Disproved (\ x -> case x of {})
(%~) SCD SCB = Disproved (\ x -> case x of {})
(%~) SCD SCC = Disproved (\ x -> case x of {})
(%~) SCD SCD = Proved Refl
(%~) SCD SCE = Disproved (\ x -> case x of {})
(%~) SCD SCF = Disproved (\ x -> case x of {})
(%~) SCD SCG = Disproved (\ x -> case x of {})
(%~) SCD SCH = Disproved (\ x -> case x of {})
(%~) SCD SCI = Disproved (\ x -> case x of {})
(%~) SCD SCJ = Disproved (\ x -> case x of {})
(%~) SCD SCK = Disproved (\ x -> case x of {})
(%~) SCD SCL = Disproved (\ x -> case x of {})
(%~) SCD SCM = Disproved (\ x -> case x of {})
(%~) SCD SCN = Disproved (\ x -> case x of {})
(%~) SCD SCO = Disproved (\ x -> case x of {})
(%~) SCD SCP = Disproved (\ x -> case x of {})
(%~) SCD SCQ = Disproved (\ x -> case x of {})
(%~) SCD SCR = Disproved (\ x -> case x of {})
(%~) SCD SCS = Disproved (\ x -> case x of {})
(%~) SCD SCT = Disproved (\ x -> case x of {})
(%~) SCD SCU = Disproved (\ x -> case x of {})
(%~) SCD SCV = Disproved (\ x -> case x of {})
(%~) SCD SCW = Disproved (\ x -> case x of {})
(%~) SCD SCX = Disproved (\ x -> case x of {})
(%~) SCD SCY = Disproved (\ x -> case x of {})
(%~) SCD SCZ = Disproved (\ x -> case x of {})
(%~) SCE SCA = Disproved (\ x -> case x of {})
(%~) SCE SCB = Disproved (\ x -> case x of {})
(%~) SCE SCC = Disproved (\ x -> case x of {})
(%~) SCE SCD = Disproved (\ x -> case x of {})
(%~) SCE SCE = Proved Refl
(%~) SCE SCF = Disproved (\ x -> case x of {})
(%~) SCE SCG = Disproved (\ x -> case x of {})
(%~) SCE SCH = Disproved (\ x -> case x of {})
(%~) SCE SCI = Disproved (\ x -> case x of {})
(%~) SCE SCJ = Disproved (\ x -> case x of {})
(%~) SCE SCK = Disproved (\ x -> case x of {})
(%~) SCE SCL = Disproved (\ x -> case x of {})
(%~) SCE SCM = Disproved (\ x -> case x of {})
(%~) SCE SCN = Disproved (\ x -> case x of {})
(%~) SCE SCO = Disproved (\ x -> case x of {})
(%~) SCE SCP = Disproved (\ x -> case x of {})
(%~) SCE SCQ = Disproved (\ x -> case x of {})
(%~) SCE SCR = Disproved (\ x -> case x of {})
(%~) SCE SCS = Disproved (\ x -> case x of {})
(%~) SCE SCT = Disproved (\ x -> case x of {})
(%~) SCE SCU = Disproved (\ x -> case x of {})
(%~) SCE SCV = Disproved (\ x -> case x of {})
(%~) SCE SCW = Disproved (\ x -> case x of {})
(%~) SCE SCX = Disproved (\ x -> case x of {})
(%~) SCE SCY = Disproved (\ x -> case x of {})
(%~) SCE SCZ = Disproved (\ x -> case x of {})
(%~) SCF SCA = Disproved (\ x -> case x of {})
(%~) SCF SCB = Disproved (\ x -> case x of {})
(%~) SCF SCC = Disproved (\ x -> case x of {})
(%~) SCF SCD = Disproved (\ x -> case x of {})
(%~) SCF SCE = Disproved (\ x -> case x of {})
(%~) SCF SCF = Proved Refl
(%~) SCF SCG = Disproved (\ x -> case x of {})
(%~) SCF SCH = Disproved (\ x -> case x of {})
(%~) SCF SCI = Disproved (\ x -> case x of {})
(%~) SCF SCJ = Disproved (\ x -> case x of {})
(%~) SCF SCK = Disproved (\ x -> case x of {})
(%~) SCF SCL = Disproved (\ x -> case x of {})
(%~) SCF SCM = Disproved (\ x -> case x of {})
(%~) SCF SCN = Disproved (\ x -> case x of {})
(%~) SCF SCO = Disproved (\ x -> case x of {})
(%~) SCF SCP = Disproved (\ x -> case x of {})
(%~) SCF SCQ = Disproved (\ x -> case x of {})
(%~) SCF SCR = Disproved (\ x -> case x of {})
(%~) SCF SCS = Disproved (\ x -> case x of {})
(%~) SCF SCT = Disproved (\ x -> case x of {})
(%~) SCF SCU = Disproved (\ x -> case x of {})
(%~) SCF SCV = Disproved (\ x -> case x of {})
(%~) SCF SCW = Disproved (\ x -> case x of {})
(%~) SCF SCX = Disproved (\ x -> case x of {})
(%~) SCF SCY = Disproved (\ x -> case x of {})
(%~) SCF SCZ = Disproved (\ x -> case x of {})
(%~) SCG SCA = Disproved (\ x -> case x of {})
(%~) SCG SCB = Disproved (\ x -> case x of {})
(%~) SCG SCC = Disproved (\ x -> case x of {})
(%~) SCG SCD = Disproved (\ x -> case x of {})
(%~) SCG SCE = Disproved (\ x -> case x of {})
(%~) SCG SCF = Disproved (\ x -> case x of {})
(%~) SCG SCG = Proved Refl
(%~) SCG SCH = Disproved (\ x -> case x of {})
(%~) SCG SCI = Disproved (\ x -> case x of {})
(%~) SCG SCJ = Disproved (\ x -> case x of {})
(%~) SCG SCK = Disproved (\ x -> case x of {})
(%~) SCG SCL = Disproved (\ x -> case x of {})
(%~) SCG SCM = Disproved (\ x -> case x of {})
(%~) SCG SCN = Disproved (\ x -> case x of {})
(%~) SCG SCO = Disproved (\ x -> case x of {})
(%~) SCG SCP = Disproved (\ x -> case x of {})
(%~) SCG SCQ = Disproved (\ x -> case x of {})
(%~) SCG SCR = Disproved (\ x -> case x of {})
(%~) SCG SCS = Disproved (\ x -> case x of {})
(%~) SCG SCT = Disproved (\ x -> case x of {})
(%~) SCG SCU = Disproved (\ x -> case x of {})
(%~) SCG SCV = Disproved (\ x -> case x of {})
(%~) SCG SCW = Disproved (\ x -> case x of {})
(%~) SCG SCX = Disproved (\ x -> case x of {})
(%~) SCG SCY = Disproved (\ x -> case x of {})
(%~) SCG SCZ = Disproved (\ x -> case x of {})
(%~) SCH SCA = Disproved (\ x -> case x of {})
(%~) SCH SCB = Disproved (\ x -> case x of {})
(%~) SCH SCC = Disproved (\ x -> case x of {})
(%~) SCH SCD = Disproved (\ x -> case x of {})
(%~) SCH SCE = Disproved (\ x -> case x of {})
(%~) SCH SCF = Disproved (\ x -> case x of {})
(%~) SCH SCG = Disproved (\ x -> case x of {})
(%~) SCH SCH = Proved Refl
(%~) SCH SCI = Disproved (\ x -> case x of {})
(%~) SCH SCJ = Disproved (\ x -> case x of {})
(%~) SCH SCK = Disproved (\ x -> case x of {})
(%~) SCH SCL = Disproved (\ x -> case x of {})
(%~) SCH SCM = Disproved (\ x -> case x of {})
(%~) SCH SCN = Disproved (\ x -> case x of {})
(%~) SCH SCO = Disproved (\ x -> case x of {})
(%~) SCH SCP = Disproved (\ x -> case x of {})
(%~) SCH SCQ = Disproved (\ x -> case x of {})
(%~) SCH SCR = Disproved (\ x -> case x of {})
(%~) SCH SCS = Disproved (\ x -> case x of {})
(%~) SCH SCT = Disproved (\ x -> case x of {})
(%~) SCH SCU = Disproved (\ x -> case x of {})
(%~) SCH SCV = Disproved (\ x -> case x of {})
(%~) SCH SCW = Disproved (\ x -> case x of {})
(%~) SCH SCX = Disproved (\ x -> case x of {})
(%~) SCH SCY = Disproved (\ x -> case x of {})
(%~) SCH SCZ = Disproved (\ x -> case x of {})
(%~) SCI SCA = Disproved (\ x -> case x of {})
(%~) SCI SCB = Disproved (\ x -> case x of {})
(%~) SCI SCC = Disproved (\ x -> case x of {})
(%~) SCI SCD = Disproved (\ x -> case x of {})
(%~) SCI SCE = Disproved (\ x -> case x of {})
(%~) SCI SCF = Disproved (\ x -> case x of {})
(%~) SCI SCG = Disproved (\ x -> case x of {})
(%~) SCI SCH = Disproved (\ x -> case x of {})
(%~) SCI SCI = Proved Refl
(%~) SCI SCJ = Disproved (\ x -> case x of {})
(%~) SCI SCK = Disproved (\ x -> case x of {})
(%~) SCI SCL = Disproved (\ x -> case x of {})
(%~) SCI SCM = Disproved (\ x -> case x of {})
(%~) SCI SCN = Disproved (\ x -> case x of {})
(%~) SCI SCO = Disproved (\ x -> case x of {})
(%~) SCI SCP = Disproved (\ x -> case x of {})
(%~) SCI SCQ = Disproved (\ x -> case x of {})
(%~) SCI SCR = Disproved (\ x -> case x of {})
(%~) SCI SCS = Disproved (\ x -> case x of {})
(%~) SCI SCT = Disproved (\ x -> case x of {})
(%~) SCI SCU = Disproved (\ x -> case x of {})
(%~) SCI SCV = Disproved (\ x -> case x of {})
(%~) SCI SCW = Disproved (\ x -> case x of {})
(%~) SCI SCX = Disproved (\ x -> case x of {})
(%~) SCI SCY = Disproved (\ x -> case x of {})
(%~) SCI SCZ = Disproved (\ x -> case x of {})
(%~) SCJ SCA = Disproved (\ x -> case x of {})
(%~) SCJ SCB = Disproved (\ x -> case x of {})
(%~) SCJ SCC = Disproved (\ x -> case x of {})
(%~) SCJ SCD = Disproved (\ x -> case x of {})
(%~) SCJ SCE = Disproved (\ x -> case x of {})
(%~) SCJ SCF = Disproved (\ x -> case x of {})
(%~) SCJ SCG = Disproved (\ x -> case x of {})
(%~) SCJ SCH = Disproved (\ x -> case x of {})
(%~) SCJ SCI = Disproved (\ x -> case x of {})
(%~) SCJ SCJ = Proved Refl
(%~) SCJ SCK = Disproved (\ x -> case x of {})
(%~) SCJ SCL = Disproved (\ x -> case x of {})
(%~) SCJ SCM = Disproved (\ x -> case x of {})
(%~) SCJ SCN = Disproved (\ x -> case x of {})
(%~) SCJ SCO = Disproved (\ x -> case x of {})
(%~) SCJ SCP = Disproved (\ x -> case x of {})
(%~) SCJ SCQ = Disproved (\ x -> case x of {})
(%~) SCJ SCR = Disproved (\ x -> case x of {})
(%~) SCJ SCS = Disproved (\ x -> case x of {})
(%~) SCJ SCT = Disproved (\ x -> case x of {})
(%~) SCJ SCU = Disproved (\ x -> case x of {})
(%~) SCJ SCV = Disproved (\ x -> case x of {})
(%~) SCJ SCW = Disproved (\ x -> case x of {})
(%~) SCJ SCX = Disproved (\ x -> case x of {})
(%~) SCJ SCY = Disproved (\ x -> case x of {})
(%~) SCJ SCZ = Disproved (\ x -> case x of {})
(%~) SCK SCA = Disproved (\ x -> case x of {})
(%~) SCK SCB = Disproved (\ x -> case x of {})
(%~) SCK SCC = Disproved (\ x -> case x of {})
(%~) SCK SCD = Disproved (\ x -> case x of {})
(%~) SCK SCE = Disproved (\ x -> case x of {})
(%~) SCK SCF = Disproved (\ x -> case x of {})
(%~) SCK SCG = Disproved (\ x -> case x of {})
(%~) SCK SCH = Disproved (\ x -> case x of {})
(%~) SCK SCI = Disproved (\ x -> case x of {})
(%~) SCK SCJ = Disproved (\ x -> case x of {})
(%~) SCK SCK = Proved Refl
(%~) SCK SCL = Disproved (\ x -> case x of {})
(%~) SCK SCM = Disproved (\ x -> case x of {})
(%~) SCK SCN = Disproved (\ x -> case x of {})
(%~) SCK SCO = Disproved (\ x -> case x of {})
(%~) SCK SCP = Disproved (\ x -> case x of {})
(%~) SCK SCQ = Disproved (\ x -> case x of {})
(%~) SCK SCR = Disproved (\ x -> case x of {})
(%~) SCK SCS = Disproved (\ x -> case x of {})
(%~) SCK SCT = Disproved (\ x -> case x of {})
(%~) SCK SCU = Disproved (\ x -> case x of {})
(%~) SCK SCV = Disproved (\ x -> case x of {})
(%~) SCK SCW = Disproved (\ x -> case x of {})
(%~) SCK SCX = Disproved (\ x -> case x of {})
(%~) SCK SCY = Disproved (\ x -> case x of {})
(%~) SCK SCZ = Disproved (\ x -> case x of {})
(%~) SCL SCA = Disproved (\ x -> case x of {})
(%~) SCL SCB = Disproved (\ x -> case x of {})
(%~) SCL SCC = Disproved (\ x -> case x of {})
(%~) SCL SCD = Disproved (\ x -> case x of {})
(%~) SCL SCE = Disproved (\ x -> case x of {})
(%~) SCL SCF = Disproved (\ x -> case x of {})
(%~) SCL SCG = Disproved (\ x -> case x of {})
(%~) SCL SCH = Disproved (\ x -> case x of {})
(%~) SCL SCI = Disproved (\ x -> case x of {})
(%~) SCL SCJ = Disproved (\ x -> case x of {})
(%~) SCL SCK = Disproved (\ x -> case x of {})
(%~) SCL SCL = Proved Refl
(%~) SCL SCM = Disproved (\ x -> case x of {})
(%~) SCL SCN = Disproved (\ x -> case x of {})
(%~) SCL SCO = Disproved (\ x -> case x of {})
(%~) SCL SCP = Disproved (\ x -> case x of {})
(%~) SCL SCQ = Disproved (\ x -> case x of {})
(%~) SCL SCR = Disproved (\ x -> case x of {})
(%~) SCL SCS = Disproved (\ x -> case x of {})
(%~) SCL SCT = Disproved (\ x -> case x of {})
(%~) SCL SCU = Disproved (\ x -> case x of {})
(%~) SCL SCV = Disproved (\ x -> case x of {})
(%~) SCL SCW = Disproved (\ x -> case x of {})
(%~) SCL SCX = Disproved (\ x -> case x of {})
(%~) SCL SCY = Disproved (\ x -> case x of {})
(%~) SCL SCZ = Disproved (\ x -> case x of {})
(%~) SCM SCA = Disproved (\ x -> case x of {})
(%~) SCM SCB = Disproved (\ x -> case x of {})
(%~) SCM SCC = Disproved (\ x -> case x of {})
(%~) SCM SCD = Disproved (\ x -> case x of {})
(%~) SCM SCE = Disproved (\ x -> case x of {})
(%~) SCM SCF = Disproved (\ x -> case x of {})
(%~) SCM SCG = Disproved (\ x -> case x of {})
(%~) SCM SCH = Disproved (\ x -> case x of {})
(%~) SCM SCI = Disproved (\ x -> case x of {})
(%~) SCM SCJ = Disproved (\ x -> case x of {})
(%~) SCM SCK = Disproved (\ x -> case x of {})
(%~) SCM SCL = Disproved (\ x -> case x of {})
(%~) SCM SCM = Proved Refl
(%~) SCM SCN = Disproved (\ x -> case x of {})
(%~) SCM SCO = Disproved (\ x -> case x of {})
(%~) SCM SCP = Disproved (\ x -> case x of {})
(%~) SCM SCQ = Disproved (\ x -> case x of {})
(%~) SCM SCR = Disproved (\ x -> case x of {})
(%~) SCM SCS = Disproved (\ x -> case x of {})
(%~) SCM SCT = Disproved (\ x -> case x of {})
(%~) SCM SCU = Disproved (\ x -> case x of {})
(%~) SCM SCV = Disproved (\ x -> case x of {})
(%~) SCM SCW = Disproved (\ x -> case x of {})
(%~) SCM SCX = Disproved (\ x -> case x of {})
(%~) SCM SCY = Disproved (\ x -> case x of {})
(%~) SCM SCZ = Disproved (\ x -> case x of {})
(%~) SCN SCA = Disproved (\ x -> case x of {})
(%~) SCN SCB = Disproved (\ x -> case x of {})
(%~) SCN SCC = Disproved (\ x -> case x of {})
(%~) SCN SCD = Disproved (\ x -> case x of {})
(%~) SCN SCE = Disproved (\ x -> case x of {})
(%~) SCN SCF = Disproved (\ x -> case x of {})
(%~) SCN SCG = Disproved (\ x -> case x of {})
(%~) SCN SCH = Disproved (\ x -> case x of {})
(%~) SCN SCI = Disproved (\ x -> case x of {})
(%~) SCN SCJ = Disproved (\ x -> case x of {})
(%~) SCN SCK = Disproved (\ x -> case x of {})
(%~) SCN SCL = Disproved (\ x -> case x of {})
(%~) SCN SCM = Disproved (\ x -> case x of {})
(%~) SCN SCN = Proved Refl
(%~) SCN SCO = Disproved (\ x -> case x of {})
(%~) SCN SCP = Disproved (\ x -> case x of {})
(%~) SCN SCQ = Disproved (\ x -> case x of {})
(%~) SCN SCR = Disproved (\ x -> case x of {})
(%~) SCN SCS = Disproved (\ x -> case x of {})
(%~) SCN SCT = Disproved (\ x -> case x of {})
(%~) SCN SCU = Disproved (\ x -> case x of {})
(%~) SCN SCV = Disproved (\ x -> case x of {})
(%~) SCN SCW = Disproved (\ x -> case x of {})
(%~) SCN SCX = Disproved (\ x -> case x of {})
(%~) SCN SCY = Disproved (\ x -> case x of {})
(%~) SCN SCZ = Disproved (\ x -> case x of {})
(%~) SCO SCA = Disproved (\ x -> case x of {})
(%~) SCO SCB = Disproved (\ x -> case x of {})
(%~) SCO SCC = Disproved (\ x -> case x of {})
(%~) SCO SCD = Disproved (\ x -> case x of {})
(%~) SCO SCE = Disproved (\ x -> case x of {})
(%~) SCO SCF = Disproved (\ x -> case x of {})
(%~) SCO SCG = Disproved (\ x -> case x of {})
(%~) SCO SCH = Disproved (\ x -> case x of {})
(%~) SCO SCI = Disproved (\ x -> case x of {})
(%~) SCO SCJ = Disproved (\ x -> case x of {})
(%~) SCO SCK = Disproved (\ x -> case x of {})
(%~) SCO SCL = Disproved (\ x -> case x of {})
(%~) SCO SCM = Disproved (\ x -> case x of {})
(%~) SCO SCN = Disproved (\ x -> case x of {})
(%~) SCO SCO = Proved Refl
(%~) SCO SCP = Disproved (\ x -> case x of {})
(%~) SCO SCQ = Disproved (\ x -> case x of {})
(%~) SCO SCR = Disproved (\ x -> case x of {})
(%~) SCO SCS = Disproved (\ x -> case x of {})
(%~) SCO SCT = Disproved (\ x -> case x of {})
(%~) SCO SCU = Disproved (\ x -> case x of {})
(%~) SCO SCV = Disproved (\ x -> case x of {})
(%~) SCO SCW = Disproved (\ x -> case x of {})
(%~) SCO SCX = Disproved (\ x -> case x of {})
(%~) SCO SCY = Disproved (\ x -> case x of {})
(%~) SCO SCZ = Disproved (\ x -> case x of {})
(%~) SCP SCA = Disproved (\ x -> case x of {})
(%~) SCP SCB = Disproved (\ x -> case x of {})
(%~) SCP SCC = Disproved (\ x -> case x of {})
(%~) SCP SCD = Disproved (\ x -> case x of {})
(%~) SCP SCE = Disproved (\ x -> case x of {})
(%~) SCP SCF = Disproved (\ x -> case x of {})
(%~) SCP SCG = Disproved (\ x -> case x of {})
(%~) SCP SCH = Disproved (\ x -> case x of {})
(%~) SCP SCI = Disproved (\ x -> case x of {})
(%~) SCP SCJ = Disproved (\ x -> case x of {})
(%~) SCP SCK = Disproved (\ x -> case x of {})
(%~) SCP SCL = Disproved (\ x -> case x of {})
(%~) SCP SCM = Disproved (\ x -> case x of {})
(%~) SCP SCN = Disproved (\ x -> case x of {})
(%~) SCP SCO = Disproved (\ x -> case x of {})
(%~) SCP SCP = Proved Refl
(%~) SCP SCQ = Disproved (\ x -> case x of {})
(%~) SCP SCR = Disproved (\ x -> case x of {})
(%~) SCP SCS = Disproved (\ x -> case x of {})
(%~) SCP SCT = Disproved (\ x -> case x of {})
(%~) SCP SCU = Disproved (\ x -> case x of {})
(%~) SCP SCV = Disproved (\ x -> case x of {})
(%~) SCP SCW = Disproved (\ x -> case x of {})
(%~) SCP SCX = Disproved (\ x -> case x of {})
(%~) SCP SCY = Disproved (\ x -> case x of {})
(%~) SCP SCZ = Disproved (\ x -> case x of {})
(%~) SCQ SCA = Disproved (\ x -> case x of {})
(%~) SCQ SCB = Disproved (\ x -> case x of {})
(%~) SCQ SCC = Disproved (\ x -> case x of {})
(%~) SCQ SCD = Disproved (\ x -> case x of {})
(%~) SCQ SCE = Disproved (\ x -> case x of {})
(%~) SCQ SCF = Disproved (\ x -> case x of {})
(%~) SCQ SCG = Disproved (\ x -> case x of {})
(%~) SCQ SCH = Disproved (\ x -> case x of {})
(%~) SCQ SCI = Disproved (\ x -> case x of {})
(%~) SCQ SCJ = Disproved (\ x -> case x of {})
(%~) SCQ SCK = Disproved (\ x -> case x of {})
(%~) SCQ SCL = Disproved (\ x -> case x of {})
(%~) SCQ SCM = Disproved (\ x -> case x of {})
(%~) SCQ SCN = Disproved (\ x -> case x of {})
(%~) SCQ SCO = Disproved (\ x -> case x of {})
(%~) SCQ SCP = Disproved (\ x -> case x of {})
(%~) SCQ SCQ = Proved Refl
(%~) SCQ SCR = Disproved (\ x -> case x of {})
(%~) SCQ SCS = Disproved (\ x -> case x of {})
(%~) SCQ SCT = Disproved (\ x -> case x of {})
(%~) SCQ SCU = Disproved (\ x -> case x of {})
(%~) SCQ SCV = Disproved (\ x -> case x of {})
(%~) SCQ SCW = Disproved (\ x -> case x of {})
(%~) SCQ SCX = Disproved (\ x -> case x of {})
(%~) SCQ SCY = Disproved (\ x -> case x of {})
(%~) SCQ SCZ = Disproved (\ x -> case x of {})
(%~) SCR SCA = Disproved (\ x -> case x of {})
(%~) SCR SCB = Disproved (\ x -> case x of {})
(%~) SCR SCC = Disproved (\ x -> case x of {})
(%~) SCR SCD = Disproved (\ x -> case x of {})
(%~) SCR SCE = Disproved (\ x -> case x of {})
(%~) SCR SCF = Disproved (\ x -> case x of {})
(%~) SCR SCG = Disproved (\ x -> case x of {})
(%~) SCR SCH = Disproved (\ x -> case x of {})
(%~) SCR SCI = Disproved (\ x -> case x of {})
(%~) SCR SCJ = Disproved (\ x -> case x of {})
(%~) SCR SCK = Disproved (\ x -> case x of {})
(%~) SCR SCL = Disproved (\ x -> case x of {})
(%~) SCR SCM = Disproved (\ x -> case x of {})
(%~) SCR SCN = Disproved (\ x -> case x of {})
(%~) SCR SCO = Disproved (\ x -> case x of {})
(%~) SCR SCP = Disproved (\ x -> case x of {})
(%~) SCR SCQ = Disproved (\ x -> case x of {})
(%~) SCR SCR = Proved Refl
(%~) SCR SCS = Disproved (\ x -> case x of {})
(%~) SCR SCT = Disproved (\ x -> case x of {})
(%~) SCR SCU = Disproved (\ x -> case x of {})
(%~) SCR SCV = Disproved (\ x -> case x of {})
(%~) SCR SCW = Disproved (\ x -> case x of {})
(%~) SCR SCX = Disproved (\ x -> case x of {})
(%~) SCR SCY = Disproved (\ x -> case x of {})
(%~) SCR SCZ = Disproved (\ x -> case x of {})
(%~) SCS SCA = Disproved (\ x -> case x of {})
(%~) SCS SCB = Disproved (\ x -> case x of {})
(%~) SCS SCC = Disproved (\ x -> case x of {})
(%~) SCS SCD = Disproved (\ x -> case x of {})
(%~) SCS SCE = Disproved (\ x -> case x of {})
(%~) SCS SCF = Disproved (\ x -> case x of {})
(%~) SCS SCG = Disproved (\ x -> case x of {})
(%~) SCS SCH = Disproved (\ x -> case x of {})
(%~) SCS SCI = Disproved (\ x -> case x of {})
(%~) SCS SCJ = Disproved (\ x -> case x of {})
(%~) SCS SCK = Disproved (\ x -> case x of {})
(%~) SCS SCL = Disproved (\ x -> case x of {})
(%~) SCS SCM = Disproved (\ x -> case x of {})
(%~) SCS SCN = Disproved (\ x -> case x of {})
(%~) SCS SCO = Disproved (\ x -> case x of {})
(%~) SCS SCP = Disproved (\ x -> case x of {})
(%~) SCS SCQ = Disproved (\ x -> case x of {})
(%~) SCS SCR = Disproved (\ x -> case x of {})
(%~) SCS SCS = Proved Refl
(%~) SCS SCT = Disproved (\ x -> case x of {})
(%~) SCS SCU = Disproved (\ x -> case x of {})
(%~) SCS SCV = Disproved (\ x -> case x of {})
(%~) SCS SCW = Disproved (\ x -> case x of {})
(%~) SCS SCX = Disproved (\ x -> case x of {})
(%~) SCS SCY = Disproved (\ x -> case x of {})
(%~) SCS SCZ = Disproved (\ x -> case x of {})
(%~) SCT SCA = Disproved (\ x -> case x of {})
(%~) SCT SCB = Disproved (\ x -> case x of {})
(%~) SCT SCC = Disproved (\ x -> case x of {})
(%~) SCT SCD = Disproved (\ x -> case x of {})
(%~) SCT SCE = Disproved (\ x -> case x of {})
(%~) SCT SCF = Disproved (\ x -> case x of {})
(%~) SCT SCG = Disproved (\ x -> case x of {})
(%~) SCT SCH = Disproved (\ x -> case x of {})
(%~) SCT SCI = Disproved (\ x -> case x of {})
(%~) SCT SCJ = Disproved (\ x -> case x of {})
(%~) SCT SCK = Disproved (\ x -> case x of {})
(%~) SCT SCL = Disproved (\ x -> case x of {})
(%~) SCT SCM = Disproved (\ x -> case x of {})
(%~) SCT SCN = Disproved (\ x -> case x of {})
(%~) SCT SCO = Disproved (\ x -> case x of {})
(%~) SCT SCP = Disproved (\ x -> case x of {})
(%~) SCT SCQ = Disproved (\ x -> case x of {})
(%~) SCT SCR = Disproved (\ x -> case x of {})
(%~) SCT SCS = Disproved (\ x -> case x of {})
(%~) SCT SCT = Proved Refl
(%~) SCT SCU = Disproved (\ x -> case x of {})
(%~) SCT SCV = Disproved (\ x -> case x of {})
(%~) SCT SCW = Disproved (\ x -> case x of {})
(%~) SCT SCX = Disproved (\ x -> case x of {})
(%~) SCT SCY = Disproved (\ x -> case x of {})
(%~) SCT SCZ = Disproved (\ x -> case x of {})
(%~) SCU SCA = Disproved (\ x -> case x of {})
(%~) SCU SCB = Disproved (\ x -> case x of {})
(%~) SCU SCC = Disproved (\ x -> case x of {})
(%~) SCU SCD = Disproved (\ x -> case x of {})
(%~) SCU SCE = Disproved (\ x -> case x of {})
(%~) SCU SCF = Disproved (\ x -> case x of {})
(%~) SCU SCG = Disproved (\ x -> case x of {})
(%~) SCU SCH = Disproved (\ x -> case x of {})
(%~) SCU SCI = Disproved (\ x -> case x of {})
(%~) SCU SCJ = Disproved (\ x -> case x of {})
(%~) SCU SCK = Disproved (\ x -> case x of {})
(%~) SCU SCL = Disproved (\ x -> case x of {})
(%~) SCU SCM = Disproved (\ x -> case x of {})
(%~) SCU SCN = Disproved (\ x -> case x of {})
(%~) SCU SCO = Disproved (\ x -> case x of {})
(%~) SCU SCP = Disproved (\ x -> case x of {})
(%~) SCU SCQ = Disproved (\ x -> case x of {})
(%~) SCU SCR = Disproved (\ x -> case x of {})
(%~) SCU SCS = Disproved (\ x -> case x of {})
(%~) SCU SCT = Disproved (\ x -> case x of {})
(%~) SCU SCU = Proved Refl
(%~) SCU SCV = Disproved (\ x -> case x of {})
(%~) SCU SCW = Disproved (\ x -> case x of {})
(%~) SCU SCX = Disproved (\ x -> case x of {})
(%~) SCU SCY = Disproved (\ x -> case x of {})
(%~) SCU SCZ = Disproved (\ x -> case x of {})
(%~) SCV SCA = Disproved (\ x -> case x of {})
(%~) SCV SCB = Disproved (\ x -> case x of {})
(%~) SCV SCC = Disproved (\ x -> case x of {})
(%~) SCV SCD = Disproved (\ x -> case x of {})
(%~) SCV SCE = Disproved (\ x -> case x of {})
(%~) SCV SCF = Disproved (\ x -> case x of {})
(%~) SCV SCG = Disproved (\ x -> case x of {})
(%~) SCV SCH = Disproved (\ x -> case x of {})
(%~) SCV SCI = Disproved (\ x -> case x of {})
(%~) SCV SCJ = Disproved (\ x -> case x of {})
(%~) SCV SCK = Disproved (\ x -> case x of {})
(%~) SCV SCL = Disproved (\ x -> case x of {})
(%~) SCV SCM = Disproved (\ x -> case x of {})
(%~) SCV SCN = Disproved (\ x -> case x of {})
(%~) SCV SCO = Disproved (\ x -> case x of {})
(%~) SCV SCP = Disproved (\ x -> case x of {})
(%~) SCV SCQ = Disproved (\ x -> case x of {})
(%~) SCV SCR = Disproved (\ x -> case x of {})
(%~) SCV SCS = Disproved (\ x -> case x of {})
(%~) SCV SCT = Disproved (\ x -> case x of {})
(%~) SCV SCU = Disproved (\ x -> case x of {})
(%~) SCV SCV = Proved Refl
(%~) SCV SCW = Disproved (\ x -> case x of {})
(%~) SCV SCX = Disproved (\ x -> case x of {})
(%~) SCV SCY = Disproved (\ x -> case x of {})
(%~) SCV SCZ = Disproved (\ x -> case x of {})
(%~) SCW SCA = Disproved (\ x -> case x of {})
(%~) SCW SCB = Disproved (\ x -> case x of {})
(%~) SCW SCC = Disproved (\ x -> case x of {})
(%~) SCW SCD = Disproved (\ x -> case x of {})
(%~) SCW SCE = Disproved (\ x -> case x of {})
(%~) SCW SCF = Disproved (\ x -> case x of {})
(%~) SCW SCG = Disproved (\ x -> case x of {})
(%~) SCW SCH = Disproved (\ x -> case x of {})
(%~) SCW SCI = Disproved (\ x -> case x of {})
(%~) SCW SCJ = Disproved (\ x -> case x of {})
(%~) SCW SCK = Disproved (\ x -> case x of {})
(%~) SCW SCL = Disproved (\ x -> case x of {})
(%~) SCW SCM = Disproved (\ x -> case x of {})
(%~) SCW SCN = Disproved (\ x -> case x of {})
(%~) SCW SCO = Disproved (\ x -> case x of {})
(%~) SCW SCP = Disproved (\ x -> case x of {})
(%~) SCW SCQ = Disproved (\ x -> case x of {})
(%~) SCW SCR = Disproved (\ x -> case x of {})
(%~) SCW SCS = Disproved (\ x -> case x of {})
(%~) SCW SCT = Disproved (\ x -> case x of {})
(%~) SCW SCU = Disproved (\ x -> case x of {})
(%~) SCW SCV = Disproved (\ x -> case x of {})
(%~) SCW SCW = Proved Refl
(%~) SCW SCX = Disproved (\ x -> case x of {})
(%~) SCW SCY = Disproved (\ x -> case x of {})
(%~) SCW SCZ = Disproved (\ x -> case x of {})
(%~) SCX SCA = Disproved (\ x -> case x of {})
(%~) SCX SCB = Disproved (\ x -> case x of {})
(%~) SCX SCC = Disproved (\ x -> case x of {})
(%~) SCX SCD = Disproved (\ x -> case x of {})
(%~) SCX SCE = Disproved (\ x -> case x of {})
(%~) SCX SCF = Disproved (\ x -> case x of {})
(%~) SCX SCG = Disproved (\ x -> case x of {})
(%~) SCX SCH = Disproved (\ x -> case x of {})
(%~) SCX SCI = Disproved (\ x -> case x of {})
(%~) SCX SCJ = Disproved (\ x -> case x of {})
(%~) SCX SCK = Disproved (\ x -> case x of {})
(%~) SCX SCL = Disproved (\ x -> case x of {})
(%~) SCX SCM = Disproved (\ x -> case x of {})
(%~) SCX SCN = Disproved (\ x -> case x of {})
(%~) SCX SCO = Disproved (\ x -> case x of {})
(%~) SCX SCP = Disproved (\ x -> case x of {})
(%~) SCX SCQ = Disproved (\ x -> case x of {})
(%~) SCX SCR = Disproved (\ x -> case x of {})
(%~) SCX SCS = Disproved (\ x -> case x of {})
(%~) SCX SCT = Disproved (\ x -> case x of {})
(%~) SCX SCU = Disproved (\ x -> case x of {})
(%~) SCX SCV = Disproved (\ x -> case x of {})
(%~) SCX SCW = Disproved (\ x -> case x of {})
(%~) SCX SCX = Proved Refl
(%~) SCX SCY = Disproved (\ x -> case x of {})
(%~) SCX SCZ = Disproved (\ x -> case x of {})
(%~) SCY SCA = Disproved (\ x -> case x of {})
(%~) SCY SCB = Disproved (\ x -> case x of {})
(%~) SCY SCC = Disproved (\ x -> case x of {})
(%~) SCY SCD = Disproved (\ x -> case x of {})
(%~) SCY SCE = Disproved (\ x -> case x of {})
(%~) SCY SCF = Disproved (\ x -> case x of {})
(%~) SCY SCG = Disproved (\ x -> case x of {})
(%~) SCY SCH = Disproved (\ x -> case x of {})
(%~) SCY SCI = Disproved (\ x -> case x of {})
(%~) SCY SCJ = Disproved (\ x -> case x of {})
(%~) SCY SCK = Disproved (\ x -> case x of {})
(%~) SCY SCL = Disproved (\ x -> case x of {})
(%~) SCY SCM = Disproved (\ x -> case x of {})
(%~) SCY SCN = Disproved (\ x -> case x of {})
(%~) SCY SCO = Disproved (\ x -> case x of {})
(%~) SCY SCP = Disproved (\ x -> case x of {})
(%~) SCY SCQ = Disproved (\ x -> case x of {})
(%~) SCY SCR = Disproved (\ x -> case x of {})
(%~) SCY SCS = Disproved (\ x -> case x of {})
(%~) SCY SCT = Disproved (\ x -> case x of {})
(%~) SCY SCU = Disproved (\ x -> case x of {})
(%~) SCY SCV = Disproved (\ x -> case x of {})
(%~) SCY SCW = Disproved (\ x -> case x of {})
(%~) SCY SCX = Disproved (\ x -> case x of {})
(%~) SCY SCY = Proved Refl
(%~) SCY SCZ = Disproved (\ x -> case x of {})
(%~) SCZ SCA = Disproved (\ x -> case x of {})
(%~) SCZ SCB = Disproved (\ x -> case x of {})
(%~) SCZ SCC = Disproved (\ x -> case x of {})
(%~) SCZ SCD = Disproved (\ x -> case x of {})
(%~) SCZ SCE = Disproved (\ x -> case x of {})
(%~) SCZ SCF = Disproved (\ x -> case x of {})
(%~) SCZ SCG = Disproved (\ x -> case x of {})
(%~) SCZ SCH = Disproved (\ x -> case x of {})
(%~) SCZ SCI = Disproved (\ x -> case x of {})
(%~) SCZ SCJ = Disproved (\ x -> case x of {})
(%~) SCZ SCK = Disproved (\ x -> case x of {})
(%~) SCZ SCL = Disproved (\ x -> case x of {})
(%~) SCZ SCM = Disproved (\ x -> case x of {})
(%~) SCZ SCN = Disproved (\ x -> case x of {})
(%~) SCZ SCO = Disproved (\ x -> case x of {})
(%~) SCZ SCP = Disproved (\ x -> case x of {})
(%~) SCZ SCQ = Disproved (\ x -> case x of {})
(%~) SCZ SCR = Disproved (\ x -> case x of {})
(%~) SCZ SCS = Disproved (\ x -> case x of {})
(%~) SCZ SCT = Disproved (\ x -> case x of {})
(%~) SCZ SCU = Disproved (\ x -> case x of {})
(%~) SCZ SCV = Disproved (\ x -> case x of {})
(%~) SCZ SCW = Disproved (\ x -> case x of {})
(%~) SCZ SCX = Disproved (\ x -> case x of {})
(%~) SCZ SCY = Disproved (\ x -> case x of {})
(%~) SCZ SCZ = Proved Refl
instance Eq (SAChar (z :: AChar)) where
(==) _ _ = True
instance GHC.Internal.Data.Type.Equality.TestEquality (SAChar :: AChar
-> Type) where
GHC.Internal.Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance GHC.Internal.Data.Type.Coercion.TestCoercion (SAChar :: AChar
-> Type) where
GHC.Internal.Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
deriving instance (Data.Singletons.ShowSing.ShowSing U,
Data.Singletons.ShowSing.ShowSing Nat) =>
Show (SU (z :: U))
deriving instance Show (SAChar (z :: AChar))
instance SingI BOOL where
sing = SBOOL
instance SingI STRING where
sing = SSTRING
instance SingI NAT where
sing = SNAT
instance (SingI n, SingI n) =>
SingI (VEC (n :: U) (n :: Nat)) where
sing = SVEC sing sing
instance SingI n => SingI1 (VEC (n :: U)) where
liftSing = SVEC sing
instance SingI2 VEC where
liftSing2 = SVEC
instance SingI (VECSym0 :: (~>) U ((~>) Nat U)) where
sing = singFun2 @VECSym0 SVEC
instance SingI d => SingI (VECSym1 (d :: U) :: (~>) Nat U) where
sing = singFun1 @(VECSym1 (d :: U)) (SVEC (sing @d))
instance SingI1 (VECSym1 :: U -> (~>) Nat U) where
liftSing (s :: Sing (d :: U))
= singFun1 @(VECSym1 (d :: U)) (SVEC s)
instance SingI CA where
sing = SCA
instance SingI CB where
sing = SCB
instance SingI CC where
sing = SCC
instance SingI CD where
sing = SCD
instance SingI CE where
sing = SCE
instance SingI CF where
sing = SCF
instance SingI CG where
sing = SCG
instance SingI CH where
sing = SCH
instance SingI CI where
sing = SCI
instance SingI CJ where
sing = SCJ
instance SingI CK where
sing = SCK
instance SingI CL where
sing = SCL
instance SingI CM where
sing = SCM
instance SingI CN where
sing = SCN
instance SingI CO where
sing = SCO
instance SingI CP where
sing = SCP
instance SingI CQ where
sing = SCQ
instance SingI CR where
sing = SCR
instance SingI CS where
sing = SCS
instance SingI CT where
sing = SCT
instance SingI CU where
sing = SCU
instance SingI CV where
sing = SCV
instance SingI CW where
sing = SCW
instance SingI CX where
sing = SCX
instance SingI CY where
sing = SCY
instance SingI CZ where
sing = SCZ
instance (SingI n, SingI n) =>
SingI (Attr (n :: [AChar]) (n :: U)) where
sing = SAttr sing sing
instance SingI n => SingI1 (Attr (n :: [AChar])) where
liftSing = SAttr sing
instance SingI2 Attr where
liftSing2 = SAttr
instance SingI (AttrSym0 :: (~>) [AChar] ((~>) U Attribute)) where
sing = singFun2 @AttrSym0 SAttr
instance SingI d =>
SingI (AttrSym1 (d :: [AChar]) :: (~>) U Attribute) where
sing = singFun1 @(AttrSym1 (d :: [AChar])) (SAttr (sing @d))
instance SingI1 (AttrSym1 :: [AChar] -> (~>) U Attribute) where
liftSing (s :: Sing (d :: [AChar]))
= singFun1 @(AttrSym1 (d :: [AChar])) (SAttr s)
instance SingI n => SingI (Sch (n :: [Attribute])) where
sing = SSch sing
instance SingI1 Sch where
liftSing = SSch
instance SingI (SchSym0 :: (~>) [Attribute] Schema) where
sing = singFun1 @SchSym0 SSch
GradingClient/Database.hs:0:0:: Splicing declarations
return [] ======>
GradingClient/Database.hs:(0,0)-(0,0): Splicing expression
cases ''Row [| r |] [| changeId (n ++ (getId r)) r |]
======>
case r of
EmptyRow _ -> changeId ((++) n (getId r)) r
ConsRow _ _ -> changeId ((++) n (getId r)) r