singletons-2.7: 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 = Zero :: Nat
type SuccSym0 :: (~>) Nat Nat
data SuccSym0 a0123456789876543210
where
SuccSym0KindInference :: SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
SuccSym0 a0123456789876543210
type instance Apply SuccSym0 a0123456789876543210 = SuccSym1 a0123456789876543210
instance SuppressUnusedWarnings SuccSym0 where
suppressUnusedWarnings = snd (((,) SuccSym0KindInference) ())
type SuccSym1 (a0123456789876543210 :: Nat) =
Succ a0123456789876543210 :: Nat
type Compare_0123456789876543210 :: Nat -> Nat -> Ordering
type family Compare_0123456789876543210 a a where
Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) NilSym0
Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) 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 a0123456789876543210
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 a0123456789876543210
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_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Compare_0123456789876543210Sym1KindInference) ())
type Compare_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) =
Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 :: Ordering
instance POrd Nat where
type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
type Equals_0123456789876543210 :: Nat -> Nat -> Bool
type family Equals_0123456789876543210 a b where
Equals_0123456789876543210 Zero Zero = TrueSym0
Equals_0123456789876543210 (Succ a) (Succ b) = (==) a b
Equals_0123456789876543210 (_ :: Nat) (_ :: Nat) = FalseSym0
instance PEq Nat where
type (==) a b = Equals_0123456789876543210 a b
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 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 @ThenCmpSym0) sThenCmp)))
SEQ))
SNil
sCompare
(SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
(SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
= (applySing
((applySing
((applySing ((singFun3 @FoldlSym0) sFoldl))
((singFun2 @ThenCmpSym0) sThenCmp)))
SEQ))
((applySing
((applySing ((singFun2 @(:@#@$)) SCons))
((applySing
((applySing ((singFun2 @CompareSym0) sCompare))
sA_0123456789876543210))
sB_0123456789876543210)))
SNil)
sCompare SZero (SSucc _) = SLT
sCompare (SSucc _) SZero = SGT
instance SEq Nat => SEq Nat where
(%==) SZero SZero = STrue
(%==) SZero (SSucc _) = SFalse
(%==) (SSucc _) SZero = SFalse
(%==) (SSucc a) (SSucc b) = ((%==) a) b
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 SDecide Nat =>
Data.Type.Equality.TestEquality (SNat :: Nat -> Type) where
Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance SDecide Nat =>
Data.Type.Coercion.TestCoercion (SNat :: Nat -> Type) where
Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
instance SingI Zero where
sing = SZero
instance SingI n => SingI (Succ (n :: Nat)) where
sing = SSucc sing
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 = BOOL :: U
type STRINGSym0 = STRING :: U
type NATSym0 = NAT :: U
type VECSym0 :: (~>) U ((~>) Nat U)
data VECSym0 a0123456789876543210
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 a0123456789876543210
where
VECSym1KindInference :: SameKind (Apply (VECSym1 a0123456789876543210) arg) (VECSym2 a0123456789876543210 arg) =>
VECSym1 a0123456789876543210 a0123456789876543210
type instance Apply (VECSym1 a0123456789876543210) a0123456789876543210 = VECSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (VECSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) VECSym1KindInference) ())
type VECSym2 (a0123456789876543210 :: U) (a0123456789876543210 :: Nat) =
VEC a0123456789876543210 a0123456789876543210 :: U
type CASym0 = CA :: AChar
type CBSym0 = CB :: AChar
type CCSym0 = CC :: AChar
type CDSym0 = CD :: AChar
type CESym0 = CE :: AChar
type CFSym0 = CF :: AChar
type CGSym0 = CG :: AChar
type CHSym0 = CH :: AChar
type CISym0 = CI :: AChar
type CJSym0 = CJ :: AChar
type CKSym0 = CK :: AChar
type CLSym0 = CL :: AChar
type CMSym0 = CM :: AChar
type CNSym0 = CN :: AChar
type COSym0 = CO :: AChar
type CPSym0 = CP :: AChar
type CQSym0 = CQ :: AChar
type CRSym0 = CR :: AChar
type CSSym0 = CS :: AChar
type CTSym0 = CT :: AChar
type CUSym0 = CU :: AChar
type CVSym0 = CV :: AChar
type CWSym0 = CW :: AChar
type CXSym0 = CX :: AChar
type CYSym0 = CY :: AChar
type CZSym0 = CZ :: AChar
type AttrSym0 :: (~>) [AChar] ((~>) U Attribute)
data AttrSym0 a0123456789876543210
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 a0123456789876543210
where
AttrSym1KindInference :: SameKind (Apply (AttrSym1 a0123456789876543210) arg) (AttrSym2 a0123456789876543210 arg) =>
AttrSym1 a0123456789876543210 a0123456789876543210
type instance Apply (AttrSym1 a0123456789876543210) a0123456789876543210 = AttrSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (AttrSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) AttrSym1KindInference) ())
type AttrSym2 (a0123456789876543210 :: [AChar]) (a0123456789876543210 :: U) =
Attr a0123456789876543210 a0123456789876543210 :: Attribute
type SchSym0 :: (~>) [Attribute] Schema
data SchSym0 a0123456789876543210
where
SchSym0KindInference :: SameKind (Apply SchSym0 arg) (SchSym1 arg) =>
SchSym0 a0123456789876543210
type instance Apply SchSym0 a0123456789876543210 = SchSym1 a0123456789876543210
instance SuppressUnusedWarnings SchSym0 where
suppressUnusedWarnings = snd (((,) SchSym0KindInference) ())
type SchSym1 (a0123456789876543210 :: [Attribute]) =
Sch a0123456789876543210 :: Schema
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_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) where
suppressUnusedWarnings
= snd
(((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym3KindInference)
())
type Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 =
Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
type family Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs where
Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs = Apply (Apply (==@#@$) name) name'
type family Case_0123456789876543210 name name' u attrs 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 a0123456789876543210
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 a0123456789876543210
where
LookupSym1KindInference :: SameKind (Apply (LookupSym1 a0123456789876543210) arg) (LookupSym2 a0123456789876543210 arg) =>
LookupSym1 a0123456789876543210 a0123456789876543210
type instance Apply (LookupSym1 a0123456789876543210) a0123456789876543210 = LookupSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (LookupSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) LookupSym1KindInference) ())
type LookupSym2 (a0123456789876543210 :: [AChar]) (a0123456789876543210 :: Schema) =
Lookup a0123456789876543210 a0123456789876543210 :: U
type OccursSym0 :: (~>) [AChar] ((~>) Schema Bool)
data OccursSym0 a0123456789876543210
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 a0123456789876543210
where
OccursSym1KindInference :: SameKind (Apply (OccursSym1 a0123456789876543210) arg) (OccursSym2 a0123456789876543210 arg) =>
OccursSym1 a0123456789876543210 a0123456789876543210
type instance Apply (OccursSym1 a0123456789876543210) a0123456789876543210 = OccursSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (OccursSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) OccursSym1KindInference) ())
type OccursSym2 (a0123456789876543210 :: [AChar]) (a0123456789876543210 :: Schema) =
Occurs a0123456789876543210 a0123456789876543210 :: Bool
type DisjointSym0 :: (~>) Schema ((~>) Schema Bool)
data DisjointSym0 a0123456789876543210
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 a0123456789876543210
where
DisjointSym1KindInference :: SameKind (Apply (DisjointSym1 a0123456789876543210) arg) (DisjointSym2 a0123456789876543210 arg) =>
DisjointSym1 a0123456789876543210 a0123456789876543210
type instance Apply (DisjointSym1 a0123456789876543210) a0123456789876543210 = DisjointSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (DisjointSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) DisjointSym1KindInference) ())
type DisjointSym2 (a0123456789876543210 :: Schema) (a0123456789876543210 :: Schema) =
Disjoint a0123456789876543210 a0123456789876543210 :: Bool
type AttrNotInSym0 :: (~>) Attribute ((~>) Schema Bool)
data AttrNotInSym0 a0123456789876543210
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 a0123456789876543210
where
AttrNotInSym1KindInference :: SameKind (Apply (AttrNotInSym1 a0123456789876543210) arg) (AttrNotInSym2 a0123456789876543210 arg) =>
AttrNotInSym1 a0123456789876543210 a0123456789876543210
type instance Apply (AttrNotInSym1 a0123456789876543210) a0123456789876543210 = AttrNotInSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (AttrNotInSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) AttrNotInSym1KindInference) ())
type AttrNotInSym2 (a0123456789876543210 :: Attribute) (a0123456789876543210 :: Schema) =
AttrNotIn a0123456789876543210 a0123456789876543210 :: Bool
type AppendSym0 :: (~>) Schema ((~>) Schema Schema)
data AppendSym0 a0123456789876543210
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 a0123456789876543210
where
AppendSym1KindInference :: SameKind (Apply (AppendSym1 a0123456789876543210) arg) (AppendSym2 a0123456789876543210 arg) =>
AppendSym1 a0123456789876543210 a0123456789876543210
type instance Apply (AppendSym1 a0123456789876543210) a0123456789876543210 = AppendSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (AppendSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) AppendSym1KindInference) ())
type AppendSym2 (a0123456789876543210 :: Schema) (a0123456789876543210 :: Schema) =
Append a0123456789876543210 a0123456789876543210 :: Schema
type Lookup :: [AChar] -> Schema -> U
type family Lookup a a 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 a 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 a 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 a 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 a where
Append (Sch s1) (Sch s2) = Apply SchSym0 (Apply (Apply (++@#@$) s1) s2)
type ShowsPrec_0123456789876543210 :: GHC.Types.Nat
-> U -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 a a a 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.Types.Nat ((~>) U ((~>) Symbol Symbol))
data ShowsPrec_0123456789876543210Sym0 a0123456789876543210
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.Types.Nat
-> (~>) U ((~>) Symbol Symbol)
data ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
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.Types.Nat
-> U -> (~>) Symbol Symbol
data ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
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_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: U) (a0123456789876543210 :: Symbol) =
ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 :: Symbol
instance PShow U where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
type ShowsPrec_0123456789876543210 :: GHC.Types.Nat
-> AChar -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 a a a 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.Types.Nat ((~>) AChar ((~>) Symbol Symbol))
data ShowsPrec_0123456789876543210Sym0 a0123456789876543210
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.Types.Nat
-> (~>) AChar ((~>) Symbol Symbol)
data ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
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.Types.Nat
-> AChar -> (~>) Symbol Symbol
data ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
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_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: AChar) (a0123456789876543210 :: Symbol) =
ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 :: Symbol
instance PShow AChar where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
type Equals_0123456789876543210 :: U -> U -> Bool
type family Equals_0123456789876543210 a b where
Equals_0123456789876543210 BOOL BOOL = TrueSym0
Equals_0123456789876543210 STRING STRING = TrueSym0
Equals_0123456789876543210 NAT NAT = TrueSym0
Equals_0123456789876543210 (VEC a a) (VEC b b) = (&&) ((==) a b) ((==) a b)
Equals_0123456789876543210 (_ :: U) (_ :: U) = FalseSym0
instance PEq U where
type (==) a b = Equals_0123456789876543210 a b
type Equals_0123456789876543210 :: AChar -> AChar -> Bool
type family Equals_0123456789876543210 a b where
Equals_0123456789876543210 CA CA = TrueSym0
Equals_0123456789876543210 CB CB = TrueSym0
Equals_0123456789876543210 CC CC = TrueSym0
Equals_0123456789876543210 CD CD = TrueSym0
Equals_0123456789876543210 CE CE = TrueSym0
Equals_0123456789876543210 CF CF = TrueSym0
Equals_0123456789876543210 CG CG = TrueSym0
Equals_0123456789876543210 CH CH = TrueSym0
Equals_0123456789876543210 CI CI = TrueSym0
Equals_0123456789876543210 CJ CJ = TrueSym0
Equals_0123456789876543210 CK CK = TrueSym0
Equals_0123456789876543210 CL CL = TrueSym0
Equals_0123456789876543210 CM CM = TrueSym0
Equals_0123456789876543210 CN CN = TrueSym0
Equals_0123456789876543210 CO CO = TrueSym0
Equals_0123456789876543210 CP CP = TrueSym0
Equals_0123456789876543210 CQ CQ = TrueSym0
Equals_0123456789876543210 CR CR = TrueSym0
Equals_0123456789876543210 CS CS = TrueSym0
Equals_0123456789876543210 CT CT = TrueSym0
Equals_0123456789876543210 CU CU = TrueSym0
Equals_0123456789876543210 CV CV = TrueSym0
Equals_0123456789876543210 CW CW = TrueSym0
Equals_0123456789876543210 CX CX = TrueSym0
Equals_0123456789876543210 CY CY = TrueSym0
Equals_0123456789876543210 CZ CZ = TrueSym0
Equals_0123456789876543210 (_ :: AChar) (_ :: AChar) = FalseSym0
instance PEq AChar where
type (==) a b = Equals_0123456789876543210 a b
sLookup ::
forall (t :: [AChar]) (t :: Schema).
Sing t -> Sing t -> Sing (Apply (Apply LookupSym0 t) t :: U)
sOccurs ::
forall (t :: [AChar]) (t :: Schema).
Sing t -> Sing t -> Sing (Apply (Apply OccursSym0 t) t :: Bool)
sDisjoint ::
forall (t :: Schema) (t :: Schema).
Sing t -> Sing t -> Sing (Apply (Apply DisjointSym0 t) t :: Bool)
sAttrNotIn ::
forall (t :: Attribute) (t :: Schema).
Sing t -> Sing t -> Sing (Apply (Apply AttrNotInSym0 t) t :: Bool)
sAppend ::
forall (t :: Schema) (t :: Schema).
Sing t -> Sing t -> Sing (Apply (Apply AppendSym0 t) t :: Schema)
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.Base.id
@(Sing (Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs) :: U)))
(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 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 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 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 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))
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 (SShow U, SShow Nat) => SShow U where
sShowsPrec ::
forall (t1 :: GHC.Types.Nat) (t2 :: U) (t3 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) 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.Types.Nat) (t2 :: AChar) (t3 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) 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 U, SEq Nat) => SEq U where
(%==) 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 a a) (SVEC b b) = ((%&&) (((%==) a) b)) (((%==) a) b)
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 (SDecide U, SDecide Nat) =>
Data.Type.Equality.TestEquality (SU :: U -> Type) where
Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance (SDecide U, SDecide Nat) =>
Data.Type.Coercion.TestCoercion (SU :: U -> Type) where
Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
instance SEq AChar where
(%==) 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 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 Data.Type.Equality.TestEquality (SAChar :: AChar
-> Type) where
Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance Data.Type.Coercion.TestCoercion (SAChar :: AChar
-> Type) where
Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
instance (Data.Singletons.ShowSing.ShowSing U,
Data.Singletons.ShowSing.ShowSing Nat) =>
Show (SU (z :: U)) where
showsPrec _ SBOOL = showString "SBOOL"
showsPrec _ SSTRING = showString "SSTRING"
showsPrec _ SNAT = showString "SNAT"
showsPrec
p_0123456789876543210
(SVEC (arg_0123456789876543210 :: Sing argTy_0123456789876543210)
(arg_0123456789876543210 :: Sing argTy_0123456789876543210))
= (showParen (((>) p_0123456789876543210) 10))
(((.) (showString "SVEC "))
(((.) ((showsPrec 11) arg_0123456789876543210))
(((.) GHC.Show.showSpace)
((showsPrec 11) arg_0123456789876543210)))) ::
(Data.Singletons.ShowSing.ShowSing' argTy_0123456789876543210,
Data.Singletons.ShowSing.ShowSing' argTy_0123456789876543210) =>
ShowS
instance Show (SAChar (z :: AChar)) where
showsPrec _ SCA = showString "SCA"
showsPrec _ SCB = showString "SCB"
showsPrec _ SCC = showString "SCC"
showsPrec _ SCD = showString "SCD"
showsPrec _ SCE = showString "SCE"
showsPrec _ SCF = showString "SCF"
showsPrec _ SCG = showString "SCG"
showsPrec _ SCH = showString "SCH"
showsPrec _ SCI = showString "SCI"
showsPrec _ SCJ = showString "SCJ"
showsPrec _ SCK = showString "SCK"
showsPrec _ SCL = showString "SCL"
showsPrec _ SCM = showString "SCM"
showsPrec _ SCN = showString "SCN"
showsPrec _ SCO = showString "SCO"
showsPrec _ SCP = showString "SCP"
showsPrec _ SCQ = showString "SCQ"
showsPrec _ SCR = showString "SCR"
showsPrec _ SCS = showString "SCS"
showsPrec _ SCT = showString "SCT"
showsPrec _ SCU = showString "SCU"
showsPrec _ SCV = showString "SCV"
showsPrec _ SCW = showString "SCW"
showsPrec _ SCX = showString "SCX"
showsPrec _ SCY = showString "SCY"
showsPrec _ SCZ = showString "SCZ"
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 (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 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 (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 SingI n => SingI (Sch (n :: [Attribute])) where
sing = SSch sing
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