GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations singletons [d| data Nat = Zero | Succ Nat deriving (Eq, Ord) |] ======> data Nat = Zero | Succ Nat deriving (Eq, Ord) type ZeroSym0 :: Nat type family ZeroSym0 :: Nat where ZeroSym0 = Zero type SuccSym0 :: (~>) Nat Nat data SuccSym0 :: (~>) Nat Nat where SuccSym0KindInference :: SameKind (Apply SuccSym0 arg) (SuccSym1 arg) => SuccSym0 a0123456789876543210 type instance Apply SuccSym0 a0123456789876543210 = Succ a0123456789876543210 instance SuppressUnusedWarnings SuccSym0 where suppressUnusedWarnings = snd (((,) SuccSym0KindInference) ()) type SuccSym1 :: Nat -> Nat type family SuccSym1 (a0123456789876543210 :: Nat) :: Nat where SuccSym1 a0123456789876543210 = Succ a0123456789876543210 type TFHelper_0123456789876543210 :: Nat -> Nat -> Bool type family TFHelper_0123456789876543210 (a :: Nat) (a :: Nat) :: Bool where TFHelper_0123456789876543210 Zero Zero = TrueSym0 TFHelper_0123456789876543210 Zero (Succ _) = FalseSym0 TFHelper_0123456789876543210 (Succ _) Zero = FalseSym0 TFHelper_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210 type TFHelper_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Bool) data TFHelper_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Bool) where TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) => TFHelper_0123456789876543210Sym0 a0123456789876543210 type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) TFHelper_0123456789876543210Sym0KindInference) ()) type TFHelper_0123456789876543210Sym1 :: Nat -> (~>) Nat Bool data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: Nat) :: (~>) Nat Bool where TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) => TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) TFHelper_0123456789876543210Sym1KindInference) ()) type TFHelper_0123456789876543210Sym2 :: Nat -> Nat -> Bool type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq Nat where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type Compare_0123456789876543210 :: Nat -> Nat -> Ordering type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 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 :: (~>) Nat ((~>) Nat Ordering) where Compare_0123456789876543210Sym0KindInference :: SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) => Compare_0123456789876543210Sym0 a0123456789876543210 type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) Compare_0123456789876543210Sym0KindInference) ()) type Compare_0123456789876543210Sym1 :: Nat -> (~>) Nat Ordering data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Nat) :: (~>) Nat Ordering where Compare_0123456789876543210Sym1KindInference :: SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) => Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) Compare_0123456789876543210Sym1KindInference) ()) type Compare_0123456789876543210Sym2 :: Nat -> Nat -> Ordering type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Ordering where Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance POrd Nat where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a data SNat :: Nat -> Type where SZero :: SNat (Zero :: Nat) SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat) type instance Sing @Nat = SNat instance SingKind Nat where type Demote Nat = Nat fromSing SZero = Zero fromSing (SSucc b) = Succ (fromSing b) toSing Zero = SomeSing SZero toSing (Succ (b :: Demote Nat)) = case toSing b :: SomeSing Nat of { SomeSing c -> SomeSing (SSucc c) } instance SEq Nat => SEq Nat where (%==) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Nat ((~>) Nat Bool) -> Type) t1) t2) (%==) SZero SZero = STrue (%==) SZero (SSucc _) = SFalse (%==) (SSucc _) SZero = SFalse (%==) (SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210)) = (applySing ((applySing ((singFun2 @(==@#@$)) (%==))) sA_0123456789876543210)) sB_0123456789876543210 instance SOrd Nat => SOrd Nat where sCompare :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering) -> Type) t1) t2) sCompare SZero SZero = (applySing ((applySing ((applySing ((singFun3 @FoldlSym0) sFoldl)) ((singFun2 @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 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 :: U type family BOOLSym0 :: U where BOOLSym0 = BOOL type STRINGSym0 :: U type family STRINGSym0 :: U where STRINGSym0 = STRING type NATSym0 :: U type family NATSym0 :: U where NATSym0 = NAT type VECSym0 :: (~>) U ((~>) Nat U) data VECSym0 :: (~>) U ((~>) Nat U) where VECSym0KindInference :: SameKind (Apply VECSym0 arg) (VECSym1 arg) => VECSym0 a0123456789876543210 type instance Apply VECSym0 a0123456789876543210 = VECSym1 a0123456789876543210 instance SuppressUnusedWarnings VECSym0 where suppressUnusedWarnings = snd (((,) VECSym0KindInference) ()) type VECSym1 :: U -> (~>) Nat U data VECSym1 (a0123456789876543210 :: U) :: (~>) Nat U where VECSym1KindInference :: SameKind (Apply (VECSym1 a0123456789876543210) arg) (VECSym2 a0123456789876543210 arg) => VECSym1 a0123456789876543210 a0123456789876543210 type instance Apply (VECSym1 a0123456789876543210) a0123456789876543210 = VEC a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (VECSym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) VECSym1KindInference) ()) type VECSym2 :: U -> Nat -> U type family VECSym2 (a0123456789876543210 :: U) (a0123456789876543210 :: Nat) :: U where VECSym2 a0123456789876543210 a0123456789876543210 = VEC a0123456789876543210 a0123456789876543210 type CASym0 :: AChar type family CASym0 :: AChar where CASym0 = CA type CBSym0 :: AChar type family CBSym0 :: AChar where CBSym0 = CB type CCSym0 :: AChar type family CCSym0 :: AChar where CCSym0 = CC type CDSym0 :: AChar type family CDSym0 :: AChar where CDSym0 = CD type CESym0 :: AChar type family CESym0 :: AChar where CESym0 = CE type CFSym0 :: AChar type family CFSym0 :: AChar where CFSym0 = CF type CGSym0 :: AChar type family CGSym0 :: AChar where CGSym0 = CG type CHSym0 :: AChar type family CHSym0 :: AChar where CHSym0 = CH type CISym0 :: AChar type family CISym0 :: AChar where CISym0 = CI type CJSym0 :: AChar type family CJSym0 :: AChar where CJSym0 = CJ type CKSym0 :: AChar type family CKSym0 :: AChar where CKSym0 = CK type CLSym0 :: AChar type family CLSym0 :: AChar where CLSym0 = CL type CMSym0 :: AChar type family CMSym0 :: AChar where CMSym0 = CM type CNSym0 :: AChar type family CNSym0 :: AChar where CNSym0 = CN type COSym0 :: AChar type family COSym0 :: AChar where COSym0 = CO type CPSym0 :: AChar type family CPSym0 :: AChar where CPSym0 = CP type CQSym0 :: AChar type family CQSym0 :: AChar where CQSym0 = CQ type CRSym0 :: AChar type family CRSym0 :: AChar where CRSym0 = CR type CSSym0 :: AChar type family CSSym0 :: AChar where CSSym0 = CS type CTSym0 :: AChar type family CTSym0 :: AChar where CTSym0 = CT type CUSym0 :: AChar type family CUSym0 :: AChar where CUSym0 = CU type CVSym0 :: AChar type family CVSym0 :: AChar where CVSym0 = CV type CWSym0 :: AChar type family CWSym0 :: AChar where CWSym0 = CW type CXSym0 :: AChar type family CXSym0 :: AChar where CXSym0 = CX type CYSym0 :: AChar type family CYSym0 :: AChar where CYSym0 = CY type CZSym0 :: AChar type family CZSym0 :: AChar where CZSym0 = CZ type AttrSym0 :: (~>) [AChar] ((~>) U Attribute) data AttrSym0 :: (~>) [AChar] ((~>) U Attribute) where AttrSym0KindInference :: SameKind (Apply AttrSym0 arg) (AttrSym1 arg) => AttrSym0 a0123456789876543210 type instance Apply AttrSym0 a0123456789876543210 = AttrSym1 a0123456789876543210 instance SuppressUnusedWarnings AttrSym0 where suppressUnusedWarnings = snd (((,) AttrSym0KindInference) ()) type AttrSym1 :: [AChar] -> (~>) U Attribute data AttrSym1 (a0123456789876543210 :: [AChar]) :: (~>) U Attribute where AttrSym1KindInference :: SameKind (Apply (AttrSym1 a0123456789876543210) arg) (AttrSym2 a0123456789876543210 arg) => AttrSym1 a0123456789876543210 a0123456789876543210 type instance Apply (AttrSym1 a0123456789876543210) a0123456789876543210 = Attr a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (AttrSym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) AttrSym1KindInference) ()) type AttrSym2 :: [AChar] -> U -> Attribute type family AttrSym2 (a0123456789876543210 :: [AChar]) (a0123456789876543210 :: U) :: Attribute where AttrSym2 a0123456789876543210 a0123456789876543210 = Attr a0123456789876543210 a0123456789876543210 type SchSym0 :: (~>) [Attribute] Schema data SchSym0 :: (~>) [Attribute] Schema where SchSym0KindInference :: SameKind (Apply SchSym0 arg) (SchSym1 arg) => SchSym0 a0123456789876543210 type instance Apply SchSym0 a0123456789876543210 = Sch a0123456789876543210 instance SuppressUnusedWarnings SchSym0 where suppressUnusedWarnings = snd (((,) SchSym0KindInference) ()) type SchSym1 :: [Attribute] -> Schema type family SchSym1 (a0123456789876543210 :: [Attribute]) :: Schema where SchSym1 a0123456789876543210 = Sch a0123456789876543210 data Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) => Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210 type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210 instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference) ()) data Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210 name'0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 arg) => Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210 name'0123456789876543210 type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) name'0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210 instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) where suppressUnusedWarnings = snd (((,) Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference) ()) data Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210 u0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 arg) => Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210 u0123456789876543210 type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210) u0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210 instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210) where suppressUnusedWarnings = snd (((,) Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference) ()) data Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym3KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 arg) => Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) where suppressUnusedWarnings = snd (((,) Let0123456789876543210Scrutinee_0123456789876543210Sym3KindInference) ()) type family Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 type family Let0123456789876543210Scrutinee_0123456789876543210 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 :: (~>) [AChar] ((~>) Schema U) where LookupSym0KindInference :: SameKind (Apply LookupSym0 arg) (LookupSym1 arg) => LookupSym0 a0123456789876543210 type instance Apply LookupSym0 a0123456789876543210 = LookupSym1 a0123456789876543210 instance SuppressUnusedWarnings LookupSym0 where suppressUnusedWarnings = snd (((,) LookupSym0KindInference) ()) type LookupSym1 :: [AChar] -> (~>) Schema U data LookupSym1 (a0123456789876543210 :: [AChar]) :: (~>) Schema U where LookupSym1KindInference :: SameKind (Apply (LookupSym1 a0123456789876543210) arg) (LookupSym2 a0123456789876543210 arg) => LookupSym1 a0123456789876543210 a0123456789876543210 type instance Apply (LookupSym1 a0123456789876543210) a0123456789876543210 = Lookup a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (LookupSym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) LookupSym1KindInference) ()) type LookupSym2 :: [AChar] -> Schema -> U type family LookupSym2 (a0123456789876543210 :: [AChar]) (a0123456789876543210 :: Schema) :: U where LookupSym2 a0123456789876543210 a0123456789876543210 = Lookup a0123456789876543210 a0123456789876543210 type OccursSym0 :: (~>) [AChar] ((~>) Schema Bool) data OccursSym0 :: (~>) [AChar] ((~>) Schema Bool) where OccursSym0KindInference :: SameKind (Apply OccursSym0 arg) (OccursSym1 arg) => OccursSym0 a0123456789876543210 type instance Apply OccursSym0 a0123456789876543210 = OccursSym1 a0123456789876543210 instance SuppressUnusedWarnings OccursSym0 where suppressUnusedWarnings = snd (((,) OccursSym0KindInference) ()) type OccursSym1 :: [AChar] -> (~>) Schema Bool data OccursSym1 (a0123456789876543210 :: [AChar]) :: (~>) Schema Bool where OccursSym1KindInference :: SameKind (Apply (OccursSym1 a0123456789876543210) arg) (OccursSym2 a0123456789876543210 arg) => OccursSym1 a0123456789876543210 a0123456789876543210 type instance Apply (OccursSym1 a0123456789876543210) a0123456789876543210 = Occurs a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (OccursSym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) OccursSym1KindInference) ()) type OccursSym2 :: [AChar] -> Schema -> Bool type family OccursSym2 (a0123456789876543210 :: [AChar]) (a0123456789876543210 :: Schema) :: Bool where OccursSym2 a0123456789876543210 a0123456789876543210 = Occurs a0123456789876543210 a0123456789876543210 type DisjointSym0 :: (~>) Schema ((~>) Schema Bool) data DisjointSym0 :: (~>) Schema ((~>) Schema Bool) where DisjointSym0KindInference :: SameKind (Apply DisjointSym0 arg) (DisjointSym1 arg) => DisjointSym0 a0123456789876543210 type instance Apply DisjointSym0 a0123456789876543210 = DisjointSym1 a0123456789876543210 instance SuppressUnusedWarnings DisjointSym0 where suppressUnusedWarnings = snd (((,) DisjointSym0KindInference) ()) type DisjointSym1 :: Schema -> (~>) Schema Bool data DisjointSym1 (a0123456789876543210 :: Schema) :: (~>) Schema Bool where DisjointSym1KindInference :: SameKind (Apply (DisjointSym1 a0123456789876543210) arg) (DisjointSym2 a0123456789876543210 arg) => DisjointSym1 a0123456789876543210 a0123456789876543210 type instance Apply (DisjointSym1 a0123456789876543210) a0123456789876543210 = Disjoint a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (DisjointSym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) DisjointSym1KindInference) ()) type DisjointSym2 :: Schema -> Schema -> Bool type family DisjointSym2 (a0123456789876543210 :: Schema) (a0123456789876543210 :: Schema) :: Bool where DisjointSym2 a0123456789876543210 a0123456789876543210 = Disjoint a0123456789876543210 a0123456789876543210 type AttrNotInSym0 :: (~>) Attribute ((~>) Schema Bool) data AttrNotInSym0 :: (~>) Attribute ((~>) Schema Bool) where AttrNotInSym0KindInference :: SameKind (Apply AttrNotInSym0 arg) (AttrNotInSym1 arg) => AttrNotInSym0 a0123456789876543210 type instance Apply AttrNotInSym0 a0123456789876543210 = AttrNotInSym1 a0123456789876543210 instance SuppressUnusedWarnings AttrNotInSym0 where suppressUnusedWarnings = snd (((,) AttrNotInSym0KindInference) ()) type AttrNotInSym1 :: Attribute -> (~>) Schema Bool data AttrNotInSym1 (a0123456789876543210 :: Attribute) :: (~>) Schema Bool where AttrNotInSym1KindInference :: SameKind (Apply (AttrNotInSym1 a0123456789876543210) arg) (AttrNotInSym2 a0123456789876543210 arg) => AttrNotInSym1 a0123456789876543210 a0123456789876543210 type instance Apply (AttrNotInSym1 a0123456789876543210) a0123456789876543210 = AttrNotIn a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (AttrNotInSym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) AttrNotInSym1KindInference) ()) type AttrNotInSym2 :: Attribute -> Schema -> Bool type family AttrNotInSym2 (a0123456789876543210 :: Attribute) (a0123456789876543210 :: Schema) :: Bool where AttrNotInSym2 a0123456789876543210 a0123456789876543210 = AttrNotIn a0123456789876543210 a0123456789876543210 type AppendSym0 :: (~>) Schema ((~>) Schema Schema) data AppendSym0 :: (~>) Schema ((~>) Schema Schema) where AppendSym0KindInference :: SameKind (Apply AppendSym0 arg) (AppendSym1 arg) => AppendSym0 a0123456789876543210 type instance Apply AppendSym0 a0123456789876543210 = AppendSym1 a0123456789876543210 instance SuppressUnusedWarnings AppendSym0 where suppressUnusedWarnings = snd (((,) AppendSym0KindInference) ()) type AppendSym1 :: Schema -> (~>) Schema Schema data AppendSym1 (a0123456789876543210 :: Schema) :: (~>) Schema Schema where AppendSym1KindInference :: SameKind (Apply (AppendSym1 a0123456789876543210) arg) (AppendSym2 a0123456789876543210 arg) => AppendSym1 a0123456789876543210 a0123456789876543210 type instance Apply (AppendSym1 a0123456789876543210) a0123456789876543210 = Append a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (AppendSym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) AppendSym1KindInference) ()) type AppendSym2 :: Schema -> Schema -> Schema type family AppendSym2 (a0123456789876543210 :: Schema) (a0123456789876543210 :: Schema) :: Schema where AppendSym2 a0123456789876543210 a0123456789876543210 = Append a0123456789876543210 a0123456789876543210 type Lookup :: [AChar] -> Schema -> U type family Lookup (a :: [AChar]) (a :: Schema) :: U where Lookup _ (Sch '[]) = UndefinedSym0 Lookup name (Sch ('(:) (Attr name' u) attrs)) = Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs) type Occurs :: [AChar] -> Schema -> Bool type family Occurs (a :: [AChar]) (a :: Schema) :: Bool where Occurs _ (Sch '[]) = FalseSym0 Occurs name (Sch ('(:) (Attr name' _) attrs)) = Apply (Apply (||@#@$) (Apply (Apply (==@#@$) name) name')) (Apply (Apply OccursSym0 name) (Apply SchSym0 attrs)) type Disjoint :: Schema -> Schema -> Bool type family Disjoint (a :: Schema) (a :: Schema) :: Bool where Disjoint (Sch '[]) _ = TrueSym0 Disjoint (Sch ('(:) h t)) s = Apply (Apply (&&@#@$) (Apply (Apply AttrNotInSym0 h) s)) (Apply (Apply DisjointSym0 (Apply SchSym0 t)) s) type AttrNotIn :: Attribute -> Schema -> Bool type family AttrNotIn (a :: Attribute) (a :: Schema) :: Bool where AttrNotIn _ (Sch '[]) = TrueSym0 AttrNotIn (Attr name u) (Sch ('(:) (Attr name' _) t)) = Apply (Apply (&&@#@$) (Apply (Apply (/=@#@$) name) name')) (Apply (Apply AttrNotInSym0 (Apply (Apply AttrSym0 name) u)) (Apply SchSym0 t)) type Append :: Schema -> Schema -> Schema type family Append (a :: Schema) (a :: Schema) :: Schema where Append (Sch s1) (Sch s2) = Apply SchSym0 (Apply (Apply (++@#@$) s1) s2) type TFHelper_0123456789876543210 :: U -> U -> Bool type family TFHelper_0123456789876543210 (a :: U) (a :: U) :: Bool where TFHelper_0123456789876543210 BOOL BOOL = TrueSym0 TFHelper_0123456789876543210 BOOL STRING = FalseSym0 TFHelper_0123456789876543210 BOOL NAT = FalseSym0 TFHelper_0123456789876543210 BOOL (VEC _ _) = FalseSym0 TFHelper_0123456789876543210 STRING BOOL = FalseSym0 TFHelper_0123456789876543210 STRING STRING = TrueSym0 TFHelper_0123456789876543210 STRING NAT = FalseSym0 TFHelper_0123456789876543210 STRING (VEC _ _) = FalseSym0 TFHelper_0123456789876543210 NAT BOOL = FalseSym0 TFHelper_0123456789876543210 NAT STRING = FalseSym0 TFHelper_0123456789876543210 NAT NAT = TrueSym0 TFHelper_0123456789876543210 NAT (VEC _ _) = FalseSym0 TFHelper_0123456789876543210 (VEC _ _) BOOL = FalseSym0 TFHelper_0123456789876543210 (VEC _ _) STRING = FalseSym0 TFHelper_0123456789876543210 (VEC _ _) NAT = FalseSym0 TFHelper_0123456789876543210 (VEC a_0123456789876543210 a_0123456789876543210) (VEC b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210) type TFHelper_0123456789876543210Sym0 :: (~>) U ((~>) U Bool) data TFHelper_0123456789876543210Sym0 :: (~>) U ((~>) U Bool) where TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) => TFHelper_0123456789876543210Sym0 a0123456789876543210 type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) TFHelper_0123456789876543210Sym0KindInference) ()) type TFHelper_0123456789876543210Sym1 :: U -> (~>) U Bool data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: U) :: (~>) U Bool where TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) => TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) TFHelper_0123456789876543210Sym1KindInference) ()) type TFHelper_0123456789876543210Sym2 :: U -> U -> Bool type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: U) (a0123456789876543210 :: U) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq U where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type ShowsPrec_0123456789876543210 :: GHC.Types.Nat -> U -> Symbol -> Symbol type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: U) (a :: Symbol) :: Symbol where ShowsPrec_0123456789876543210 _ BOOL a_0123456789876543210 = Apply (Apply ShowStringSym0 "BOOL") a_0123456789876543210 ShowsPrec_0123456789876543210 _ STRING a_0123456789876543210 = Apply (Apply ShowStringSym0 "STRING") a_0123456789876543210 ShowsPrec_0123456789876543210 _ NAT a_0123456789876543210 = Apply (Apply ShowStringSym0 "NAT") a_0123456789876543210 ShowsPrec_0123456789876543210 p_0123456789876543210 (VEC arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "VEC ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210 type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Types.Nat ((~>) U ((~>) Symbol Symbol)) data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Types.Nat ((~>) U ((~>) Symbol Symbol)) where ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) => ShowsPrec_0123456789876543210Sym0 a0123456789876543210 type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ()) type ShowsPrec_0123456789876543210Sym1 :: GHC.Types.Nat -> (~>) U ((~>) Symbol Symbol) data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: (~>) U ((~>) Symbol Symbol) where ShowsPrec_0123456789876543210Sym1KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) => ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ()) type ShowsPrec_0123456789876543210Sym2 :: GHC.Types.Nat -> U -> (~>) Symbol Symbol data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: U) :: (~>) Symbol Symbol where ShowsPrec_0123456789876543210Sym2KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) => ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ()) type ShowsPrec_0123456789876543210Sym3 :: GHC.Types.Nat -> U -> Symbol -> Symbol type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: U) (a0123456789876543210 :: Symbol) :: Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow U where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a type ShowsPrec_0123456789876543210 :: GHC.Types.Nat -> AChar -> Symbol -> Symbol type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: AChar) (a :: Symbol) :: Symbol where ShowsPrec_0123456789876543210 _ CA a_0123456789876543210 = Apply (Apply ShowStringSym0 "CA") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CB a_0123456789876543210 = Apply (Apply ShowStringSym0 "CB") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CC a_0123456789876543210 = Apply (Apply ShowStringSym0 "CC") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CD a_0123456789876543210 = Apply (Apply ShowStringSym0 "CD") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CE a_0123456789876543210 = Apply (Apply ShowStringSym0 "CE") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CF a_0123456789876543210 = Apply (Apply ShowStringSym0 "CF") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CG a_0123456789876543210 = Apply (Apply ShowStringSym0 "CG") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CH a_0123456789876543210 = Apply (Apply ShowStringSym0 "CH") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CI a_0123456789876543210 = Apply (Apply ShowStringSym0 "CI") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CJ a_0123456789876543210 = Apply (Apply ShowStringSym0 "CJ") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CK a_0123456789876543210 = Apply (Apply ShowStringSym0 "CK") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CL a_0123456789876543210 = Apply (Apply ShowStringSym0 "CL") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CM a_0123456789876543210 = Apply (Apply ShowStringSym0 "CM") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CN a_0123456789876543210 = Apply (Apply ShowStringSym0 "CN") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CO a_0123456789876543210 = Apply (Apply ShowStringSym0 "CO") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CP a_0123456789876543210 = Apply (Apply ShowStringSym0 "CP") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CQ a_0123456789876543210 = Apply (Apply ShowStringSym0 "CQ") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CR a_0123456789876543210 = Apply (Apply ShowStringSym0 "CR") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CS a_0123456789876543210 = Apply (Apply ShowStringSym0 "CS") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CT a_0123456789876543210 = Apply (Apply ShowStringSym0 "CT") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CU a_0123456789876543210 = Apply (Apply ShowStringSym0 "CU") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CV a_0123456789876543210 = Apply (Apply ShowStringSym0 "CV") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CW a_0123456789876543210 = Apply (Apply ShowStringSym0 "CW") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CX a_0123456789876543210 = Apply (Apply ShowStringSym0 "CX") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CY a_0123456789876543210 = Apply (Apply ShowStringSym0 "CY") a_0123456789876543210 ShowsPrec_0123456789876543210 _ CZ a_0123456789876543210 = Apply (Apply ShowStringSym0 "CZ") a_0123456789876543210 type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Types.Nat ((~>) AChar ((~>) Symbol Symbol)) data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Types.Nat ((~>) AChar ((~>) Symbol Symbol)) where ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) => ShowsPrec_0123456789876543210Sym0 a0123456789876543210 type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ()) type ShowsPrec_0123456789876543210Sym1 :: GHC.Types.Nat -> (~>) AChar ((~>) Symbol Symbol) data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: (~>) AChar ((~>) Symbol Symbol) where ShowsPrec_0123456789876543210Sym1KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) => ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ()) type ShowsPrec_0123456789876543210Sym2 :: GHC.Types.Nat -> AChar -> (~>) Symbol Symbol data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: AChar) :: (~>) Symbol Symbol where ShowsPrec_0123456789876543210Sym2KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) => ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210 type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ()) type ShowsPrec_0123456789876543210Sym3 :: GHC.Types.Nat -> AChar -> Symbol -> Symbol type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: AChar) (a0123456789876543210 :: Symbol) :: Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow AChar where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a type TFHelper_0123456789876543210 :: AChar -> AChar -> Bool type family TFHelper_0123456789876543210 (a :: AChar) (a :: AChar) :: Bool where TFHelper_0123456789876543210 CA CA = TrueSym0 TFHelper_0123456789876543210 CA CB = FalseSym0 TFHelper_0123456789876543210 CA CC = FalseSym0 TFHelper_0123456789876543210 CA CD = FalseSym0 TFHelper_0123456789876543210 CA CE = FalseSym0 TFHelper_0123456789876543210 CA CF = FalseSym0 TFHelper_0123456789876543210 CA CG = FalseSym0 TFHelper_0123456789876543210 CA CH = FalseSym0 TFHelper_0123456789876543210 CA CI = FalseSym0 TFHelper_0123456789876543210 CA CJ = FalseSym0 TFHelper_0123456789876543210 CA CK = FalseSym0 TFHelper_0123456789876543210 CA CL = FalseSym0 TFHelper_0123456789876543210 CA CM = FalseSym0 TFHelper_0123456789876543210 CA CN = FalseSym0 TFHelper_0123456789876543210 CA CO = FalseSym0 TFHelper_0123456789876543210 CA CP = FalseSym0 TFHelper_0123456789876543210 CA CQ = FalseSym0 TFHelper_0123456789876543210 CA CR = FalseSym0 TFHelper_0123456789876543210 CA CS = FalseSym0 TFHelper_0123456789876543210 CA CT = FalseSym0 TFHelper_0123456789876543210 CA CU = FalseSym0 TFHelper_0123456789876543210 CA CV = FalseSym0 TFHelper_0123456789876543210 CA CW = FalseSym0 TFHelper_0123456789876543210 CA CX = FalseSym0 TFHelper_0123456789876543210 CA CY = FalseSym0 TFHelper_0123456789876543210 CA CZ = FalseSym0 TFHelper_0123456789876543210 CB CA = FalseSym0 TFHelper_0123456789876543210 CB CB = TrueSym0 TFHelper_0123456789876543210 CB CC = FalseSym0 TFHelper_0123456789876543210 CB CD = FalseSym0 TFHelper_0123456789876543210 CB CE = FalseSym0 TFHelper_0123456789876543210 CB CF = FalseSym0 TFHelper_0123456789876543210 CB CG = FalseSym0 TFHelper_0123456789876543210 CB CH = FalseSym0 TFHelper_0123456789876543210 CB CI = FalseSym0 TFHelper_0123456789876543210 CB CJ = FalseSym0 TFHelper_0123456789876543210 CB CK = FalseSym0 TFHelper_0123456789876543210 CB CL = FalseSym0 TFHelper_0123456789876543210 CB CM = FalseSym0 TFHelper_0123456789876543210 CB CN = FalseSym0 TFHelper_0123456789876543210 CB CO = FalseSym0 TFHelper_0123456789876543210 CB CP = FalseSym0 TFHelper_0123456789876543210 CB CQ = FalseSym0 TFHelper_0123456789876543210 CB CR = FalseSym0 TFHelper_0123456789876543210 CB CS = FalseSym0 TFHelper_0123456789876543210 CB CT = FalseSym0 TFHelper_0123456789876543210 CB CU = FalseSym0 TFHelper_0123456789876543210 CB CV = FalseSym0 TFHelper_0123456789876543210 CB CW = FalseSym0 TFHelper_0123456789876543210 CB CX = FalseSym0 TFHelper_0123456789876543210 CB CY = FalseSym0 TFHelper_0123456789876543210 CB CZ = FalseSym0 TFHelper_0123456789876543210 CC CA = FalseSym0 TFHelper_0123456789876543210 CC CB = FalseSym0 TFHelper_0123456789876543210 CC CC = TrueSym0 TFHelper_0123456789876543210 CC CD = FalseSym0 TFHelper_0123456789876543210 CC CE = FalseSym0 TFHelper_0123456789876543210 CC CF = FalseSym0 TFHelper_0123456789876543210 CC CG = FalseSym0 TFHelper_0123456789876543210 CC CH = FalseSym0 TFHelper_0123456789876543210 CC CI = FalseSym0 TFHelper_0123456789876543210 CC CJ = FalseSym0 TFHelper_0123456789876543210 CC CK = FalseSym0 TFHelper_0123456789876543210 CC CL = FalseSym0 TFHelper_0123456789876543210 CC CM = FalseSym0 TFHelper_0123456789876543210 CC CN = FalseSym0 TFHelper_0123456789876543210 CC CO = FalseSym0 TFHelper_0123456789876543210 CC CP = FalseSym0 TFHelper_0123456789876543210 CC CQ = FalseSym0 TFHelper_0123456789876543210 CC CR = FalseSym0 TFHelper_0123456789876543210 CC CS = FalseSym0 TFHelper_0123456789876543210 CC CT = FalseSym0 TFHelper_0123456789876543210 CC CU = FalseSym0 TFHelper_0123456789876543210 CC CV = FalseSym0 TFHelper_0123456789876543210 CC CW = FalseSym0 TFHelper_0123456789876543210 CC CX = FalseSym0 TFHelper_0123456789876543210 CC CY = FalseSym0 TFHelper_0123456789876543210 CC CZ = FalseSym0 TFHelper_0123456789876543210 CD CA = FalseSym0 TFHelper_0123456789876543210 CD CB = FalseSym0 TFHelper_0123456789876543210 CD CC = FalseSym0 TFHelper_0123456789876543210 CD CD = TrueSym0 TFHelper_0123456789876543210 CD CE = FalseSym0 TFHelper_0123456789876543210 CD CF = FalseSym0 TFHelper_0123456789876543210 CD CG = FalseSym0 TFHelper_0123456789876543210 CD CH = FalseSym0 TFHelper_0123456789876543210 CD CI = FalseSym0 TFHelper_0123456789876543210 CD CJ = FalseSym0 TFHelper_0123456789876543210 CD CK = FalseSym0 TFHelper_0123456789876543210 CD CL = FalseSym0 TFHelper_0123456789876543210 CD CM = FalseSym0 TFHelper_0123456789876543210 CD CN = FalseSym0 TFHelper_0123456789876543210 CD CO = FalseSym0 TFHelper_0123456789876543210 CD CP = FalseSym0 TFHelper_0123456789876543210 CD CQ = FalseSym0 TFHelper_0123456789876543210 CD CR = FalseSym0 TFHelper_0123456789876543210 CD CS = FalseSym0 TFHelper_0123456789876543210 CD CT = FalseSym0 TFHelper_0123456789876543210 CD CU = FalseSym0 TFHelper_0123456789876543210 CD CV = FalseSym0 TFHelper_0123456789876543210 CD CW = FalseSym0 TFHelper_0123456789876543210 CD CX = FalseSym0 TFHelper_0123456789876543210 CD CY = FalseSym0 TFHelper_0123456789876543210 CD CZ = FalseSym0 TFHelper_0123456789876543210 CE CA = FalseSym0 TFHelper_0123456789876543210 CE CB = FalseSym0 TFHelper_0123456789876543210 CE CC = FalseSym0 TFHelper_0123456789876543210 CE CD = FalseSym0 TFHelper_0123456789876543210 CE CE = TrueSym0 TFHelper_0123456789876543210 CE CF = FalseSym0 TFHelper_0123456789876543210 CE CG = FalseSym0 TFHelper_0123456789876543210 CE CH = FalseSym0 TFHelper_0123456789876543210 CE CI = FalseSym0 TFHelper_0123456789876543210 CE CJ = FalseSym0 TFHelper_0123456789876543210 CE CK = FalseSym0 TFHelper_0123456789876543210 CE CL = FalseSym0 TFHelper_0123456789876543210 CE CM = FalseSym0 TFHelper_0123456789876543210 CE CN = FalseSym0 TFHelper_0123456789876543210 CE CO = FalseSym0 TFHelper_0123456789876543210 CE CP = FalseSym0 TFHelper_0123456789876543210 CE CQ = FalseSym0 TFHelper_0123456789876543210 CE CR = FalseSym0 TFHelper_0123456789876543210 CE CS = FalseSym0 TFHelper_0123456789876543210 CE CT = FalseSym0 TFHelper_0123456789876543210 CE CU = FalseSym0 TFHelper_0123456789876543210 CE CV = FalseSym0 TFHelper_0123456789876543210 CE CW = FalseSym0 TFHelper_0123456789876543210 CE CX = FalseSym0 TFHelper_0123456789876543210 CE CY = FalseSym0 TFHelper_0123456789876543210 CE CZ = FalseSym0 TFHelper_0123456789876543210 CF CA = FalseSym0 TFHelper_0123456789876543210 CF CB = FalseSym0 TFHelper_0123456789876543210 CF CC = FalseSym0 TFHelper_0123456789876543210 CF CD = FalseSym0 TFHelper_0123456789876543210 CF CE = FalseSym0 TFHelper_0123456789876543210 CF CF = TrueSym0 TFHelper_0123456789876543210 CF CG = FalseSym0 TFHelper_0123456789876543210 CF CH = FalseSym0 TFHelper_0123456789876543210 CF CI = FalseSym0 TFHelper_0123456789876543210 CF CJ = FalseSym0 TFHelper_0123456789876543210 CF CK = FalseSym0 TFHelper_0123456789876543210 CF CL = FalseSym0 TFHelper_0123456789876543210 CF CM = FalseSym0 TFHelper_0123456789876543210 CF CN = FalseSym0 TFHelper_0123456789876543210 CF CO = FalseSym0 TFHelper_0123456789876543210 CF CP = FalseSym0 TFHelper_0123456789876543210 CF CQ = FalseSym0 TFHelper_0123456789876543210 CF CR = FalseSym0 TFHelper_0123456789876543210 CF CS = FalseSym0 TFHelper_0123456789876543210 CF CT = FalseSym0 TFHelper_0123456789876543210 CF CU = FalseSym0 TFHelper_0123456789876543210 CF CV = FalseSym0 TFHelper_0123456789876543210 CF CW = FalseSym0 TFHelper_0123456789876543210 CF CX = FalseSym0 TFHelper_0123456789876543210 CF CY = FalseSym0 TFHelper_0123456789876543210 CF CZ = FalseSym0 TFHelper_0123456789876543210 CG CA = FalseSym0 TFHelper_0123456789876543210 CG CB = FalseSym0 TFHelper_0123456789876543210 CG CC = FalseSym0 TFHelper_0123456789876543210 CG CD = FalseSym0 TFHelper_0123456789876543210 CG CE = FalseSym0 TFHelper_0123456789876543210 CG CF = FalseSym0 TFHelper_0123456789876543210 CG CG = TrueSym0 TFHelper_0123456789876543210 CG CH = FalseSym0 TFHelper_0123456789876543210 CG CI = FalseSym0 TFHelper_0123456789876543210 CG CJ = FalseSym0 TFHelper_0123456789876543210 CG CK = FalseSym0 TFHelper_0123456789876543210 CG CL = FalseSym0 TFHelper_0123456789876543210 CG CM = FalseSym0 TFHelper_0123456789876543210 CG CN = FalseSym0 TFHelper_0123456789876543210 CG CO = FalseSym0 TFHelper_0123456789876543210 CG CP = FalseSym0 TFHelper_0123456789876543210 CG CQ = FalseSym0 TFHelper_0123456789876543210 CG CR = FalseSym0 TFHelper_0123456789876543210 CG CS = FalseSym0 TFHelper_0123456789876543210 CG CT = FalseSym0 TFHelper_0123456789876543210 CG CU = FalseSym0 TFHelper_0123456789876543210 CG CV = FalseSym0 TFHelper_0123456789876543210 CG CW = FalseSym0 TFHelper_0123456789876543210 CG CX = FalseSym0 TFHelper_0123456789876543210 CG CY = FalseSym0 TFHelper_0123456789876543210 CG CZ = FalseSym0 TFHelper_0123456789876543210 CH CA = FalseSym0 TFHelper_0123456789876543210 CH CB = FalseSym0 TFHelper_0123456789876543210 CH CC = FalseSym0 TFHelper_0123456789876543210 CH CD = FalseSym0 TFHelper_0123456789876543210 CH CE = FalseSym0 TFHelper_0123456789876543210 CH CF = FalseSym0 TFHelper_0123456789876543210 CH CG = FalseSym0 TFHelper_0123456789876543210 CH CH = TrueSym0 TFHelper_0123456789876543210 CH CI = FalseSym0 TFHelper_0123456789876543210 CH CJ = FalseSym0 TFHelper_0123456789876543210 CH CK = FalseSym0 TFHelper_0123456789876543210 CH CL = FalseSym0 TFHelper_0123456789876543210 CH CM = FalseSym0 TFHelper_0123456789876543210 CH CN = FalseSym0 TFHelper_0123456789876543210 CH CO = FalseSym0 TFHelper_0123456789876543210 CH CP = FalseSym0 TFHelper_0123456789876543210 CH CQ = FalseSym0 TFHelper_0123456789876543210 CH CR = FalseSym0 TFHelper_0123456789876543210 CH CS = FalseSym0 TFHelper_0123456789876543210 CH CT = FalseSym0 TFHelper_0123456789876543210 CH CU = FalseSym0 TFHelper_0123456789876543210 CH CV = FalseSym0 TFHelper_0123456789876543210 CH CW = FalseSym0 TFHelper_0123456789876543210 CH CX = FalseSym0 TFHelper_0123456789876543210 CH CY = FalseSym0 TFHelper_0123456789876543210 CH CZ = FalseSym0 TFHelper_0123456789876543210 CI CA = FalseSym0 TFHelper_0123456789876543210 CI CB = FalseSym0 TFHelper_0123456789876543210 CI CC = FalseSym0 TFHelper_0123456789876543210 CI CD = FalseSym0 TFHelper_0123456789876543210 CI CE = FalseSym0 TFHelper_0123456789876543210 CI CF = FalseSym0 TFHelper_0123456789876543210 CI CG = FalseSym0 TFHelper_0123456789876543210 CI CH = FalseSym0 TFHelper_0123456789876543210 CI CI = TrueSym0 TFHelper_0123456789876543210 CI CJ = FalseSym0 TFHelper_0123456789876543210 CI CK = FalseSym0 TFHelper_0123456789876543210 CI CL = FalseSym0 TFHelper_0123456789876543210 CI CM = FalseSym0 TFHelper_0123456789876543210 CI CN = FalseSym0 TFHelper_0123456789876543210 CI CO = FalseSym0 TFHelper_0123456789876543210 CI CP = FalseSym0 TFHelper_0123456789876543210 CI CQ = FalseSym0 TFHelper_0123456789876543210 CI CR = FalseSym0 TFHelper_0123456789876543210 CI CS = FalseSym0 TFHelper_0123456789876543210 CI CT = FalseSym0 TFHelper_0123456789876543210 CI CU = FalseSym0 TFHelper_0123456789876543210 CI CV = FalseSym0 TFHelper_0123456789876543210 CI CW = FalseSym0 TFHelper_0123456789876543210 CI CX = FalseSym0 TFHelper_0123456789876543210 CI CY = FalseSym0 TFHelper_0123456789876543210 CI CZ = FalseSym0 TFHelper_0123456789876543210 CJ CA = FalseSym0 TFHelper_0123456789876543210 CJ CB = FalseSym0 TFHelper_0123456789876543210 CJ CC = FalseSym0 TFHelper_0123456789876543210 CJ CD = FalseSym0 TFHelper_0123456789876543210 CJ CE = FalseSym0 TFHelper_0123456789876543210 CJ CF = FalseSym0 TFHelper_0123456789876543210 CJ CG = FalseSym0 TFHelper_0123456789876543210 CJ CH = FalseSym0 TFHelper_0123456789876543210 CJ CI = FalseSym0 TFHelper_0123456789876543210 CJ CJ = TrueSym0 TFHelper_0123456789876543210 CJ CK = FalseSym0 TFHelper_0123456789876543210 CJ CL = FalseSym0 TFHelper_0123456789876543210 CJ CM = FalseSym0 TFHelper_0123456789876543210 CJ CN = FalseSym0 TFHelper_0123456789876543210 CJ CO = FalseSym0 TFHelper_0123456789876543210 CJ CP = FalseSym0 TFHelper_0123456789876543210 CJ CQ = FalseSym0 TFHelper_0123456789876543210 CJ CR = FalseSym0 TFHelper_0123456789876543210 CJ CS = FalseSym0 TFHelper_0123456789876543210 CJ CT = FalseSym0 TFHelper_0123456789876543210 CJ CU = FalseSym0 TFHelper_0123456789876543210 CJ CV = FalseSym0 TFHelper_0123456789876543210 CJ CW = FalseSym0 TFHelper_0123456789876543210 CJ CX = FalseSym0 TFHelper_0123456789876543210 CJ CY = FalseSym0 TFHelper_0123456789876543210 CJ CZ = FalseSym0 TFHelper_0123456789876543210 CK CA = FalseSym0 TFHelper_0123456789876543210 CK CB = FalseSym0 TFHelper_0123456789876543210 CK CC = FalseSym0 TFHelper_0123456789876543210 CK CD = FalseSym0 TFHelper_0123456789876543210 CK CE = FalseSym0 TFHelper_0123456789876543210 CK CF = FalseSym0 TFHelper_0123456789876543210 CK CG = FalseSym0 TFHelper_0123456789876543210 CK CH = FalseSym0 TFHelper_0123456789876543210 CK CI = FalseSym0 TFHelper_0123456789876543210 CK CJ = FalseSym0 TFHelper_0123456789876543210 CK CK = TrueSym0 TFHelper_0123456789876543210 CK CL = FalseSym0 TFHelper_0123456789876543210 CK CM = FalseSym0 TFHelper_0123456789876543210 CK CN = FalseSym0 TFHelper_0123456789876543210 CK CO = FalseSym0 TFHelper_0123456789876543210 CK CP = FalseSym0 TFHelper_0123456789876543210 CK CQ = FalseSym0 TFHelper_0123456789876543210 CK CR = FalseSym0 TFHelper_0123456789876543210 CK CS = FalseSym0 TFHelper_0123456789876543210 CK CT = FalseSym0 TFHelper_0123456789876543210 CK CU = FalseSym0 TFHelper_0123456789876543210 CK CV = FalseSym0 TFHelper_0123456789876543210 CK CW = FalseSym0 TFHelper_0123456789876543210 CK CX = FalseSym0 TFHelper_0123456789876543210 CK CY = FalseSym0 TFHelper_0123456789876543210 CK CZ = FalseSym0 TFHelper_0123456789876543210 CL CA = FalseSym0 TFHelper_0123456789876543210 CL CB = FalseSym0 TFHelper_0123456789876543210 CL CC = FalseSym0 TFHelper_0123456789876543210 CL CD = FalseSym0 TFHelper_0123456789876543210 CL CE = FalseSym0 TFHelper_0123456789876543210 CL CF = FalseSym0 TFHelper_0123456789876543210 CL CG = FalseSym0 TFHelper_0123456789876543210 CL CH = FalseSym0 TFHelper_0123456789876543210 CL CI = FalseSym0 TFHelper_0123456789876543210 CL CJ = FalseSym0 TFHelper_0123456789876543210 CL CK = FalseSym0 TFHelper_0123456789876543210 CL CL = TrueSym0 TFHelper_0123456789876543210 CL CM = FalseSym0 TFHelper_0123456789876543210 CL CN = FalseSym0 TFHelper_0123456789876543210 CL CO = FalseSym0 TFHelper_0123456789876543210 CL CP = FalseSym0 TFHelper_0123456789876543210 CL CQ = FalseSym0 TFHelper_0123456789876543210 CL CR = FalseSym0 TFHelper_0123456789876543210 CL CS = FalseSym0 TFHelper_0123456789876543210 CL CT = FalseSym0 TFHelper_0123456789876543210 CL CU = FalseSym0 TFHelper_0123456789876543210 CL CV = FalseSym0 TFHelper_0123456789876543210 CL CW = FalseSym0 TFHelper_0123456789876543210 CL CX = FalseSym0 TFHelper_0123456789876543210 CL CY = FalseSym0 TFHelper_0123456789876543210 CL CZ = FalseSym0 TFHelper_0123456789876543210 CM CA = FalseSym0 TFHelper_0123456789876543210 CM CB = FalseSym0 TFHelper_0123456789876543210 CM CC = FalseSym0 TFHelper_0123456789876543210 CM CD = FalseSym0 TFHelper_0123456789876543210 CM CE = FalseSym0 TFHelper_0123456789876543210 CM CF = FalseSym0 TFHelper_0123456789876543210 CM CG = FalseSym0 TFHelper_0123456789876543210 CM CH = FalseSym0 TFHelper_0123456789876543210 CM CI = FalseSym0 TFHelper_0123456789876543210 CM CJ = FalseSym0 TFHelper_0123456789876543210 CM CK = FalseSym0 TFHelper_0123456789876543210 CM CL = FalseSym0 TFHelper_0123456789876543210 CM CM = TrueSym0 TFHelper_0123456789876543210 CM CN = FalseSym0 TFHelper_0123456789876543210 CM CO = FalseSym0 TFHelper_0123456789876543210 CM CP = FalseSym0 TFHelper_0123456789876543210 CM CQ = FalseSym0 TFHelper_0123456789876543210 CM CR = FalseSym0 TFHelper_0123456789876543210 CM CS = FalseSym0 TFHelper_0123456789876543210 CM CT = FalseSym0 TFHelper_0123456789876543210 CM CU = FalseSym0 TFHelper_0123456789876543210 CM CV = FalseSym0 TFHelper_0123456789876543210 CM CW = FalseSym0 TFHelper_0123456789876543210 CM CX = FalseSym0 TFHelper_0123456789876543210 CM CY = FalseSym0 TFHelper_0123456789876543210 CM CZ = FalseSym0 TFHelper_0123456789876543210 CN CA = FalseSym0 TFHelper_0123456789876543210 CN CB = FalseSym0 TFHelper_0123456789876543210 CN CC = FalseSym0 TFHelper_0123456789876543210 CN CD = FalseSym0 TFHelper_0123456789876543210 CN CE = FalseSym0 TFHelper_0123456789876543210 CN CF = FalseSym0 TFHelper_0123456789876543210 CN CG = FalseSym0 TFHelper_0123456789876543210 CN CH = FalseSym0 TFHelper_0123456789876543210 CN CI = FalseSym0 TFHelper_0123456789876543210 CN CJ = FalseSym0 TFHelper_0123456789876543210 CN CK = FalseSym0 TFHelper_0123456789876543210 CN CL = FalseSym0 TFHelper_0123456789876543210 CN CM = FalseSym0 TFHelper_0123456789876543210 CN CN = TrueSym0 TFHelper_0123456789876543210 CN CO = FalseSym0 TFHelper_0123456789876543210 CN CP = FalseSym0 TFHelper_0123456789876543210 CN CQ = FalseSym0 TFHelper_0123456789876543210 CN CR = FalseSym0 TFHelper_0123456789876543210 CN CS = FalseSym0 TFHelper_0123456789876543210 CN CT = FalseSym0 TFHelper_0123456789876543210 CN CU = FalseSym0 TFHelper_0123456789876543210 CN CV = FalseSym0 TFHelper_0123456789876543210 CN CW = FalseSym0 TFHelper_0123456789876543210 CN CX = FalseSym0 TFHelper_0123456789876543210 CN CY = FalseSym0 TFHelper_0123456789876543210 CN CZ = FalseSym0 TFHelper_0123456789876543210 CO CA = FalseSym0 TFHelper_0123456789876543210 CO CB = FalseSym0 TFHelper_0123456789876543210 CO CC = FalseSym0 TFHelper_0123456789876543210 CO CD = FalseSym0 TFHelper_0123456789876543210 CO CE = FalseSym0 TFHelper_0123456789876543210 CO CF = FalseSym0 TFHelper_0123456789876543210 CO CG = FalseSym0 TFHelper_0123456789876543210 CO CH = FalseSym0 TFHelper_0123456789876543210 CO CI = FalseSym0 TFHelper_0123456789876543210 CO CJ = FalseSym0 TFHelper_0123456789876543210 CO CK = FalseSym0 TFHelper_0123456789876543210 CO CL = FalseSym0 TFHelper_0123456789876543210 CO CM = FalseSym0 TFHelper_0123456789876543210 CO CN = FalseSym0 TFHelper_0123456789876543210 CO CO = TrueSym0 TFHelper_0123456789876543210 CO CP = FalseSym0 TFHelper_0123456789876543210 CO CQ = FalseSym0 TFHelper_0123456789876543210 CO CR = FalseSym0 TFHelper_0123456789876543210 CO CS = FalseSym0 TFHelper_0123456789876543210 CO CT = FalseSym0 TFHelper_0123456789876543210 CO CU = FalseSym0 TFHelper_0123456789876543210 CO CV = FalseSym0 TFHelper_0123456789876543210 CO CW = FalseSym0 TFHelper_0123456789876543210 CO CX = FalseSym0 TFHelper_0123456789876543210 CO CY = FalseSym0 TFHelper_0123456789876543210 CO CZ = FalseSym0 TFHelper_0123456789876543210 CP CA = FalseSym0 TFHelper_0123456789876543210 CP CB = FalseSym0 TFHelper_0123456789876543210 CP CC = FalseSym0 TFHelper_0123456789876543210 CP CD = FalseSym0 TFHelper_0123456789876543210 CP CE = FalseSym0 TFHelper_0123456789876543210 CP CF = FalseSym0 TFHelper_0123456789876543210 CP CG = FalseSym0 TFHelper_0123456789876543210 CP CH = FalseSym0 TFHelper_0123456789876543210 CP CI = FalseSym0 TFHelper_0123456789876543210 CP CJ = FalseSym0 TFHelper_0123456789876543210 CP CK = FalseSym0 TFHelper_0123456789876543210 CP CL = FalseSym0 TFHelper_0123456789876543210 CP CM = FalseSym0 TFHelper_0123456789876543210 CP CN = FalseSym0 TFHelper_0123456789876543210 CP CO = FalseSym0 TFHelper_0123456789876543210 CP CP = TrueSym0 TFHelper_0123456789876543210 CP CQ = FalseSym0 TFHelper_0123456789876543210 CP CR = FalseSym0 TFHelper_0123456789876543210 CP CS = FalseSym0 TFHelper_0123456789876543210 CP CT = FalseSym0 TFHelper_0123456789876543210 CP CU = FalseSym0 TFHelper_0123456789876543210 CP CV = FalseSym0 TFHelper_0123456789876543210 CP CW = FalseSym0 TFHelper_0123456789876543210 CP CX = FalseSym0 TFHelper_0123456789876543210 CP CY = FalseSym0 TFHelper_0123456789876543210 CP CZ = FalseSym0 TFHelper_0123456789876543210 CQ CA = FalseSym0 TFHelper_0123456789876543210 CQ CB = FalseSym0 TFHelper_0123456789876543210 CQ CC = FalseSym0 TFHelper_0123456789876543210 CQ CD = FalseSym0 TFHelper_0123456789876543210 CQ CE = FalseSym0 TFHelper_0123456789876543210 CQ CF = FalseSym0 TFHelper_0123456789876543210 CQ CG = FalseSym0 TFHelper_0123456789876543210 CQ CH = FalseSym0 TFHelper_0123456789876543210 CQ CI = FalseSym0 TFHelper_0123456789876543210 CQ CJ = FalseSym0 TFHelper_0123456789876543210 CQ CK = FalseSym0 TFHelper_0123456789876543210 CQ CL = FalseSym0 TFHelper_0123456789876543210 CQ CM = FalseSym0 TFHelper_0123456789876543210 CQ CN = FalseSym0 TFHelper_0123456789876543210 CQ CO = FalseSym0 TFHelper_0123456789876543210 CQ CP = FalseSym0 TFHelper_0123456789876543210 CQ CQ = TrueSym0 TFHelper_0123456789876543210 CQ CR = FalseSym0 TFHelper_0123456789876543210 CQ CS = FalseSym0 TFHelper_0123456789876543210 CQ CT = FalseSym0 TFHelper_0123456789876543210 CQ CU = FalseSym0 TFHelper_0123456789876543210 CQ CV = FalseSym0 TFHelper_0123456789876543210 CQ CW = FalseSym0 TFHelper_0123456789876543210 CQ CX = FalseSym0 TFHelper_0123456789876543210 CQ CY = FalseSym0 TFHelper_0123456789876543210 CQ CZ = FalseSym0 TFHelper_0123456789876543210 CR CA = FalseSym0 TFHelper_0123456789876543210 CR CB = FalseSym0 TFHelper_0123456789876543210 CR CC = FalseSym0 TFHelper_0123456789876543210 CR CD = FalseSym0 TFHelper_0123456789876543210 CR CE = FalseSym0 TFHelper_0123456789876543210 CR CF = FalseSym0 TFHelper_0123456789876543210 CR CG = FalseSym0 TFHelper_0123456789876543210 CR CH = FalseSym0 TFHelper_0123456789876543210 CR CI = FalseSym0 TFHelper_0123456789876543210 CR CJ = FalseSym0 TFHelper_0123456789876543210 CR CK = FalseSym0 TFHelper_0123456789876543210 CR CL = FalseSym0 TFHelper_0123456789876543210 CR CM = FalseSym0 TFHelper_0123456789876543210 CR CN = FalseSym0 TFHelper_0123456789876543210 CR CO = FalseSym0 TFHelper_0123456789876543210 CR CP = FalseSym0 TFHelper_0123456789876543210 CR CQ = FalseSym0 TFHelper_0123456789876543210 CR CR = TrueSym0 TFHelper_0123456789876543210 CR CS = FalseSym0 TFHelper_0123456789876543210 CR CT = FalseSym0 TFHelper_0123456789876543210 CR CU = FalseSym0 TFHelper_0123456789876543210 CR CV = FalseSym0 TFHelper_0123456789876543210 CR CW = FalseSym0 TFHelper_0123456789876543210 CR CX = FalseSym0 TFHelper_0123456789876543210 CR CY = FalseSym0 TFHelper_0123456789876543210 CR CZ = FalseSym0 TFHelper_0123456789876543210 CS CA = FalseSym0 TFHelper_0123456789876543210 CS CB = FalseSym0 TFHelper_0123456789876543210 CS CC = FalseSym0 TFHelper_0123456789876543210 CS CD = FalseSym0 TFHelper_0123456789876543210 CS CE = FalseSym0 TFHelper_0123456789876543210 CS CF = FalseSym0 TFHelper_0123456789876543210 CS CG = FalseSym0 TFHelper_0123456789876543210 CS CH = FalseSym0 TFHelper_0123456789876543210 CS CI = FalseSym0 TFHelper_0123456789876543210 CS CJ = FalseSym0 TFHelper_0123456789876543210 CS CK = FalseSym0 TFHelper_0123456789876543210 CS CL = FalseSym0 TFHelper_0123456789876543210 CS CM = FalseSym0 TFHelper_0123456789876543210 CS CN = FalseSym0 TFHelper_0123456789876543210 CS CO = FalseSym0 TFHelper_0123456789876543210 CS CP = FalseSym0 TFHelper_0123456789876543210 CS CQ = FalseSym0 TFHelper_0123456789876543210 CS CR = FalseSym0 TFHelper_0123456789876543210 CS CS = TrueSym0 TFHelper_0123456789876543210 CS CT = FalseSym0 TFHelper_0123456789876543210 CS CU = FalseSym0 TFHelper_0123456789876543210 CS CV = FalseSym0 TFHelper_0123456789876543210 CS CW = FalseSym0 TFHelper_0123456789876543210 CS CX = FalseSym0 TFHelper_0123456789876543210 CS CY = FalseSym0 TFHelper_0123456789876543210 CS CZ = FalseSym0 TFHelper_0123456789876543210 CT CA = FalseSym0 TFHelper_0123456789876543210 CT CB = FalseSym0 TFHelper_0123456789876543210 CT CC = FalseSym0 TFHelper_0123456789876543210 CT CD = FalseSym0 TFHelper_0123456789876543210 CT CE = FalseSym0 TFHelper_0123456789876543210 CT CF = FalseSym0 TFHelper_0123456789876543210 CT CG = FalseSym0 TFHelper_0123456789876543210 CT CH = FalseSym0 TFHelper_0123456789876543210 CT CI = FalseSym0 TFHelper_0123456789876543210 CT CJ = FalseSym0 TFHelper_0123456789876543210 CT CK = FalseSym0 TFHelper_0123456789876543210 CT CL = FalseSym0 TFHelper_0123456789876543210 CT CM = FalseSym0 TFHelper_0123456789876543210 CT CN = FalseSym0 TFHelper_0123456789876543210 CT CO = FalseSym0 TFHelper_0123456789876543210 CT CP = FalseSym0 TFHelper_0123456789876543210 CT CQ = FalseSym0 TFHelper_0123456789876543210 CT CR = FalseSym0 TFHelper_0123456789876543210 CT CS = FalseSym0 TFHelper_0123456789876543210 CT CT = TrueSym0 TFHelper_0123456789876543210 CT CU = FalseSym0 TFHelper_0123456789876543210 CT CV = FalseSym0 TFHelper_0123456789876543210 CT CW = FalseSym0 TFHelper_0123456789876543210 CT CX = FalseSym0 TFHelper_0123456789876543210 CT CY = FalseSym0 TFHelper_0123456789876543210 CT CZ = FalseSym0 TFHelper_0123456789876543210 CU CA = FalseSym0 TFHelper_0123456789876543210 CU CB = FalseSym0 TFHelper_0123456789876543210 CU CC = FalseSym0 TFHelper_0123456789876543210 CU CD = FalseSym0 TFHelper_0123456789876543210 CU CE = FalseSym0 TFHelper_0123456789876543210 CU CF = FalseSym0 TFHelper_0123456789876543210 CU CG = FalseSym0 TFHelper_0123456789876543210 CU CH = FalseSym0 TFHelper_0123456789876543210 CU CI = FalseSym0 TFHelper_0123456789876543210 CU CJ = FalseSym0 TFHelper_0123456789876543210 CU CK = FalseSym0 TFHelper_0123456789876543210 CU CL = FalseSym0 TFHelper_0123456789876543210 CU CM = FalseSym0 TFHelper_0123456789876543210 CU CN = FalseSym0 TFHelper_0123456789876543210 CU CO = FalseSym0 TFHelper_0123456789876543210 CU CP = FalseSym0 TFHelper_0123456789876543210 CU CQ = FalseSym0 TFHelper_0123456789876543210 CU CR = FalseSym0 TFHelper_0123456789876543210 CU CS = FalseSym0 TFHelper_0123456789876543210 CU CT = FalseSym0 TFHelper_0123456789876543210 CU CU = TrueSym0 TFHelper_0123456789876543210 CU CV = FalseSym0 TFHelper_0123456789876543210 CU CW = FalseSym0 TFHelper_0123456789876543210 CU CX = FalseSym0 TFHelper_0123456789876543210 CU CY = FalseSym0 TFHelper_0123456789876543210 CU CZ = FalseSym0 TFHelper_0123456789876543210 CV CA = FalseSym0 TFHelper_0123456789876543210 CV CB = FalseSym0 TFHelper_0123456789876543210 CV CC = FalseSym0 TFHelper_0123456789876543210 CV CD = FalseSym0 TFHelper_0123456789876543210 CV CE = FalseSym0 TFHelper_0123456789876543210 CV CF = FalseSym0 TFHelper_0123456789876543210 CV CG = FalseSym0 TFHelper_0123456789876543210 CV CH = FalseSym0 TFHelper_0123456789876543210 CV CI = FalseSym0 TFHelper_0123456789876543210 CV CJ = FalseSym0 TFHelper_0123456789876543210 CV CK = FalseSym0 TFHelper_0123456789876543210 CV CL = FalseSym0 TFHelper_0123456789876543210 CV CM = FalseSym0 TFHelper_0123456789876543210 CV CN = FalseSym0 TFHelper_0123456789876543210 CV CO = FalseSym0 TFHelper_0123456789876543210 CV CP = FalseSym0 TFHelper_0123456789876543210 CV CQ = FalseSym0 TFHelper_0123456789876543210 CV CR = FalseSym0 TFHelper_0123456789876543210 CV CS = FalseSym0 TFHelper_0123456789876543210 CV CT = FalseSym0 TFHelper_0123456789876543210 CV CU = FalseSym0 TFHelper_0123456789876543210 CV CV = TrueSym0 TFHelper_0123456789876543210 CV CW = FalseSym0 TFHelper_0123456789876543210 CV CX = FalseSym0 TFHelper_0123456789876543210 CV CY = FalseSym0 TFHelper_0123456789876543210 CV CZ = FalseSym0 TFHelper_0123456789876543210 CW CA = FalseSym0 TFHelper_0123456789876543210 CW CB = FalseSym0 TFHelper_0123456789876543210 CW CC = FalseSym0 TFHelper_0123456789876543210 CW CD = FalseSym0 TFHelper_0123456789876543210 CW CE = FalseSym0 TFHelper_0123456789876543210 CW CF = FalseSym0 TFHelper_0123456789876543210 CW CG = FalseSym0 TFHelper_0123456789876543210 CW CH = FalseSym0 TFHelper_0123456789876543210 CW CI = FalseSym0 TFHelper_0123456789876543210 CW CJ = FalseSym0 TFHelper_0123456789876543210 CW CK = FalseSym0 TFHelper_0123456789876543210 CW CL = FalseSym0 TFHelper_0123456789876543210 CW CM = FalseSym0 TFHelper_0123456789876543210 CW CN = FalseSym0 TFHelper_0123456789876543210 CW CO = FalseSym0 TFHelper_0123456789876543210 CW CP = FalseSym0 TFHelper_0123456789876543210 CW CQ = FalseSym0 TFHelper_0123456789876543210 CW CR = FalseSym0 TFHelper_0123456789876543210 CW CS = FalseSym0 TFHelper_0123456789876543210 CW CT = FalseSym0 TFHelper_0123456789876543210 CW CU = FalseSym0 TFHelper_0123456789876543210 CW CV = FalseSym0 TFHelper_0123456789876543210 CW CW = TrueSym0 TFHelper_0123456789876543210 CW CX = FalseSym0 TFHelper_0123456789876543210 CW CY = FalseSym0 TFHelper_0123456789876543210 CW CZ = FalseSym0 TFHelper_0123456789876543210 CX CA = FalseSym0 TFHelper_0123456789876543210 CX CB = FalseSym0 TFHelper_0123456789876543210 CX CC = FalseSym0 TFHelper_0123456789876543210 CX CD = FalseSym0 TFHelper_0123456789876543210 CX CE = FalseSym0 TFHelper_0123456789876543210 CX CF = FalseSym0 TFHelper_0123456789876543210 CX CG = FalseSym0 TFHelper_0123456789876543210 CX CH = FalseSym0 TFHelper_0123456789876543210 CX CI = FalseSym0 TFHelper_0123456789876543210 CX CJ = FalseSym0 TFHelper_0123456789876543210 CX CK = FalseSym0 TFHelper_0123456789876543210 CX CL = FalseSym0 TFHelper_0123456789876543210 CX CM = FalseSym0 TFHelper_0123456789876543210 CX CN = FalseSym0 TFHelper_0123456789876543210 CX CO = FalseSym0 TFHelper_0123456789876543210 CX CP = FalseSym0 TFHelper_0123456789876543210 CX CQ = FalseSym0 TFHelper_0123456789876543210 CX CR = FalseSym0 TFHelper_0123456789876543210 CX CS = FalseSym0 TFHelper_0123456789876543210 CX CT = FalseSym0 TFHelper_0123456789876543210 CX CU = FalseSym0 TFHelper_0123456789876543210 CX CV = FalseSym0 TFHelper_0123456789876543210 CX CW = FalseSym0 TFHelper_0123456789876543210 CX CX = TrueSym0 TFHelper_0123456789876543210 CX CY = FalseSym0 TFHelper_0123456789876543210 CX CZ = FalseSym0 TFHelper_0123456789876543210 CY CA = FalseSym0 TFHelper_0123456789876543210 CY CB = FalseSym0 TFHelper_0123456789876543210 CY CC = FalseSym0 TFHelper_0123456789876543210 CY CD = FalseSym0 TFHelper_0123456789876543210 CY CE = FalseSym0 TFHelper_0123456789876543210 CY CF = FalseSym0 TFHelper_0123456789876543210 CY CG = FalseSym0 TFHelper_0123456789876543210 CY CH = FalseSym0 TFHelper_0123456789876543210 CY CI = FalseSym0 TFHelper_0123456789876543210 CY CJ = FalseSym0 TFHelper_0123456789876543210 CY CK = FalseSym0 TFHelper_0123456789876543210 CY CL = FalseSym0 TFHelper_0123456789876543210 CY CM = FalseSym0 TFHelper_0123456789876543210 CY CN = FalseSym0 TFHelper_0123456789876543210 CY CO = FalseSym0 TFHelper_0123456789876543210 CY CP = FalseSym0 TFHelper_0123456789876543210 CY CQ = FalseSym0 TFHelper_0123456789876543210 CY CR = FalseSym0 TFHelper_0123456789876543210 CY CS = FalseSym0 TFHelper_0123456789876543210 CY CT = FalseSym0 TFHelper_0123456789876543210 CY CU = FalseSym0 TFHelper_0123456789876543210 CY CV = FalseSym0 TFHelper_0123456789876543210 CY CW = FalseSym0 TFHelper_0123456789876543210 CY CX = FalseSym0 TFHelper_0123456789876543210 CY CY = TrueSym0 TFHelper_0123456789876543210 CY CZ = FalseSym0 TFHelper_0123456789876543210 CZ CA = FalseSym0 TFHelper_0123456789876543210 CZ CB = FalseSym0 TFHelper_0123456789876543210 CZ CC = FalseSym0 TFHelper_0123456789876543210 CZ CD = FalseSym0 TFHelper_0123456789876543210 CZ CE = FalseSym0 TFHelper_0123456789876543210 CZ CF = FalseSym0 TFHelper_0123456789876543210 CZ CG = FalseSym0 TFHelper_0123456789876543210 CZ CH = FalseSym0 TFHelper_0123456789876543210 CZ CI = FalseSym0 TFHelper_0123456789876543210 CZ CJ = FalseSym0 TFHelper_0123456789876543210 CZ CK = FalseSym0 TFHelper_0123456789876543210 CZ CL = FalseSym0 TFHelper_0123456789876543210 CZ CM = FalseSym0 TFHelper_0123456789876543210 CZ CN = FalseSym0 TFHelper_0123456789876543210 CZ CO = FalseSym0 TFHelper_0123456789876543210 CZ CP = FalseSym0 TFHelper_0123456789876543210 CZ CQ = FalseSym0 TFHelper_0123456789876543210 CZ CR = FalseSym0 TFHelper_0123456789876543210 CZ CS = FalseSym0 TFHelper_0123456789876543210 CZ CT = FalseSym0 TFHelper_0123456789876543210 CZ CU = FalseSym0 TFHelper_0123456789876543210 CZ CV = FalseSym0 TFHelper_0123456789876543210 CZ CW = FalseSym0 TFHelper_0123456789876543210 CZ CX = FalseSym0 TFHelper_0123456789876543210 CZ CY = FalseSym0 TFHelper_0123456789876543210 CZ CZ = TrueSym0 type TFHelper_0123456789876543210Sym0 :: (~>) AChar ((~>) AChar Bool) data TFHelper_0123456789876543210Sym0 :: (~>) AChar ((~>) AChar Bool) where TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) => TFHelper_0123456789876543210Sym0 a0123456789876543210 type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) TFHelper_0123456789876543210Sym0KindInference) ()) type TFHelper_0123456789876543210Sym1 :: AChar -> (~>) AChar Bool data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: AChar) :: (~>) AChar Bool where TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) => TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210 type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) TFHelper_0123456789876543210Sym1KindInference) ()) type TFHelper_0123456789876543210Sym2 :: AChar -> AChar -> Bool type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: AChar) (a0123456789876543210 :: AChar) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq AChar where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a sLookup :: forall (t :: [AChar]) (t :: Schema). Sing t -> Sing t -> Sing (Apply (Apply LookupSym0 t) t :: U) 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 (SEq U, SEq Nat) => SEq U where (%==) :: forall (t1 :: U) (t2 :: U). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun U ((~>) U Bool) -> Type) t1) t2) (%==) SBOOL SBOOL = STrue (%==) SBOOL SSTRING = SFalse (%==) SBOOL SNAT = SFalse (%==) SBOOL (SVEC _ _) = SFalse (%==) SSTRING SBOOL = SFalse (%==) SSTRING SSTRING = STrue (%==) SSTRING SNAT = SFalse (%==) SSTRING (SVEC _ _) = SFalse (%==) SNAT SBOOL = SFalse (%==) SNAT SSTRING = SFalse (%==) SNAT SNAT = STrue (%==) SNAT (SVEC _ _) = SFalse (%==) (SVEC _ _) SBOOL = SFalse (%==) (SVEC _ _) SSTRING = SFalse (%==) (SVEC _ _) SNAT = SFalse (%==) (SVEC (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SVEC (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = (applySing ((applySing ((singFun2 @(&&@#@$)) (%&&))) ((applySing ((applySing ((singFun2 @(==@#@$)) (%==))) sA_0123456789876543210)) sB_0123456789876543210))) ((applySing ((applySing ((singFun2 @(==@#@$)) (%==))) sA_0123456789876543210)) sB_0123456789876543210) instance (SShow U, SShow Nat) => SShow U where sShowsPrec :: forall (t1 :: GHC.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 AChar where (%==) :: forall (t1 :: AChar) (t2 :: AChar). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun AChar ((~>) AChar Bool) -> Type) t1) t2) (%==) SCA SCA = STrue (%==) SCA SCB = SFalse (%==) SCA SCC = SFalse (%==) SCA SCD = SFalse (%==) SCA SCE = SFalse (%==) SCA SCF = SFalse (%==) SCA SCG = SFalse (%==) SCA SCH = SFalse (%==) SCA SCI = SFalse (%==) SCA SCJ = SFalse (%==) SCA SCK = SFalse (%==) SCA SCL = SFalse (%==) SCA SCM = SFalse (%==) SCA SCN = SFalse (%==) SCA SCO = SFalse (%==) SCA SCP = SFalse (%==) SCA SCQ = SFalse (%==) SCA SCR = SFalse (%==) SCA SCS = SFalse (%==) SCA SCT = SFalse (%==) SCA SCU = SFalse (%==) SCA SCV = SFalse (%==) SCA SCW = SFalse (%==) SCA SCX = SFalse (%==) SCA SCY = SFalse (%==) SCA SCZ = SFalse (%==) SCB SCA = SFalse (%==) SCB SCB = STrue (%==) SCB SCC = SFalse (%==) SCB SCD = SFalse (%==) SCB SCE = SFalse (%==) SCB SCF = SFalse (%==) SCB SCG = SFalse (%==) SCB SCH = SFalse (%==) SCB SCI = SFalse (%==) SCB SCJ = SFalse (%==) SCB SCK = SFalse (%==) SCB SCL = SFalse (%==) SCB SCM = SFalse (%==) SCB SCN = SFalse (%==) SCB SCO = SFalse (%==) SCB SCP = SFalse (%==) SCB SCQ = SFalse (%==) SCB SCR = SFalse (%==) SCB SCS = SFalse (%==) SCB SCT = SFalse (%==) SCB SCU = SFalse (%==) SCB SCV = SFalse (%==) SCB SCW = SFalse (%==) SCB SCX = SFalse (%==) SCB SCY = SFalse (%==) SCB SCZ = SFalse (%==) SCC SCA = SFalse (%==) SCC SCB = SFalse (%==) SCC SCC = STrue (%==) SCC SCD = SFalse (%==) SCC SCE = SFalse (%==) SCC SCF = SFalse (%==) SCC SCG = SFalse (%==) SCC SCH = SFalse (%==) SCC SCI = SFalse (%==) SCC SCJ = SFalse (%==) SCC SCK = SFalse (%==) SCC SCL = SFalse (%==) SCC SCM = SFalse (%==) SCC SCN = SFalse (%==) SCC SCO = SFalse (%==) SCC SCP = SFalse (%==) SCC SCQ = SFalse (%==) SCC SCR = SFalse (%==) SCC SCS = SFalse (%==) SCC SCT = SFalse (%==) SCC SCU = SFalse (%==) SCC SCV = SFalse (%==) SCC SCW = SFalse (%==) SCC SCX = SFalse (%==) SCC SCY = SFalse (%==) SCC SCZ = SFalse (%==) SCD SCA = SFalse (%==) SCD SCB = SFalse (%==) SCD SCC = SFalse (%==) SCD SCD = STrue (%==) SCD SCE = SFalse (%==) SCD SCF = SFalse (%==) SCD SCG = SFalse (%==) SCD SCH = SFalse (%==) SCD SCI = SFalse (%==) SCD SCJ = SFalse (%==) SCD SCK = SFalse (%==) SCD SCL = SFalse (%==) SCD SCM = SFalse (%==) SCD SCN = SFalse (%==) SCD SCO = SFalse (%==) SCD SCP = SFalse (%==) SCD SCQ = SFalse (%==) SCD SCR = SFalse (%==) SCD SCS = SFalse (%==) SCD SCT = SFalse (%==) SCD SCU = SFalse (%==) SCD SCV = SFalse (%==) SCD SCW = SFalse (%==) SCD SCX = SFalse (%==) SCD SCY = SFalse (%==) SCD SCZ = SFalse (%==) SCE SCA = SFalse (%==) SCE SCB = SFalse (%==) SCE SCC = SFalse (%==) SCE SCD = SFalse (%==) SCE SCE = STrue (%==) SCE SCF = SFalse (%==) SCE SCG = SFalse (%==) SCE SCH = SFalse (%==) SCE SCI = SFalse (%==) SCE SCJ = SFalse (%==) SCE SCK = SFalse (%==) SCE SCL = SFalse (%==) SCE SCM = SFalse (%==) SCE SCN = SFalse (%==) SCE SCO = SFalse (%==) SCE SCP = SFalse (%==) SCE SCQ = SFalse (%==) SCE SCR = SFalse (%==) SCE SCS = SFalse (%==) SCE SCT = SFalse (%==) SCE SCU = SFalse (%==) SCE SCV = SFalse (%==) SCE SCW = SFalse (%==) SCE SCX = SFalse (%==) SCE SCY = SFalse (%==) SCE SCZ = SFalse (%==) SCF SCA = SFalse (%==) SCF SCB = SFalse (%==) SCF SCC = SFalse (%==) SCF SCD = SFalse (%==) SCF SCE = SFalse (%==) SCF SCF = STrue (%==) SCF SCG = SFalse (%==) SCF SCH = SFalse (%==) SCF SCI = SFalse (%==) SCF SCJ = SFalse (%==) SCF SCK = SFalse (%==) SCF SCL = SFalse (%==) SCF SCM = SFalse (%==) SCF SCN = SFalse (%==) SCF SCO = SFalse (%==) SCF SCP = SFalse (%==) SCF SCQ = SFalse (%==) SCF SCR = SFalse (%==) SCF SCS = SFalse (%==) SCF SCT = SFalse (%==) SCF SCU = SFalse (%==) SCF SCV = SFalse (%==) SCF SCW = SFalse (%==) SCF SCX = SFalse (%==) SCF SCY = SFalse (%==) SCF SCZ = SFalse (%==) SCG SCA = SFalse (%==) SCG SCB = SFalse (%==) SCG SCC = SFalse (%==) SCG SCD = SFalse (%==) SCG SCE = SFalse (%==) SCG SCF = SFalse (%==) SCG SCG = STrue (%==) SCG SCH = SFalse (%==) SCG SCI = SFalse (%==) SCG SCJ = SFalse (%==) SCG SCK = SFalse (%==) SCG SCL = SFalse (%==) SCG SCM = SFalse (%==) SCG SCN = SFalse (%==) SCG SCO = SFalse (%==) SCG SCP = SFalse (%==) SCG SCQ = SFalse (%==) SCG SCR = SFalse (%==) SCG SCS = SFalse (%==) SCG SCT = SFalse (%==) SCG SCU = SFalse (%==) SCG SCV = SFalse (%==) SCG SCW = SFalse (%==) SCG SCX = SFalse (%==) SCG SCY = SFalse (%==) SCG SCZ = SFalse (%==) SCH SCA = SFalse (%==) SCH SCB = SFalse (%==) SCH SCC = SFalse (%==) SCH SCD = SFalse (%==) SCH SCE = SFalse (%==) SCH SCF = SFalse (%==) SCH SCG = SFalse (%==) SCH SCH = STrue (%==) SCH SCI = SFalse (%==) SCH SCJ = SFalse (%==) SCH SCK = SFalse (%==) SCH SCL = SFalse (%==) SCH SCM = SFalse (%==) SCH SCN = SFalse (%==) SCH SCO = SFalse (%==) SCH SCP = SFalse (%==) SCH SCQ = SFalse (%==) SCH SCR = SFalse (%==) SCH SCS = SFalse (%==) SCH SCT = SFalse (%==) SCH SCU = SFalse (%==) SCH SCV = SFalse (%==) SCH SCW = SFalse (%==) SCH SCX = SFalse (%==) SCH SCY = SFalse (%==) SCH SCZ = SFalse (%==) SCI SCA = SFalse (%==) SCI SCB = SFalse (%==) SCI SCC = SFalse (%==) SCI SCD = SFalse (%==) SCI SCE = SFalse (%==) SCI SCF = SFalse (%==) SCI SCG = SFalse (%==) SCI SCH = SFalse (%==) SCI SCI = STrue (%==) SCI SCJ = SFalse (%==) SCI SCK = SFalse (%==) SCI SCL = SFalse (%==) SCI SCM = SFalse (%==) SCI SCN = SFalse (%==) SCI SCO = SFalse (%==) SCI SCP = SFalse (%==) SCI SCQ = SFalse (%==) SCI SCR = SFalse (%==) SCI SCS = SFalse (%==) SCI SCT = SFalse (%==) SCI SCU = SFalse (%==) SCI SCV = SFalse (%==) SCI SCW = SFalse (%==) SCI SCX = SFalse (%==) SCI SCY = SFalse (%==) SCI SCZ = SFalse (%==) SCJ SCA = SFalse (%==) SCJ SCB = SFalse (%==) SCJ SCC = SFalse (%==) SCJ SCD = SFalse (%==) SCJ SCE = SFalse (%==) SCJ SCF = SFalse (%==) SCJ SCG = SFalse (%==) SCJ SCH = SFalse (%==) SCJ SCI = SFalse (%==) SCJ SCJ = STrue (%==) SCJ SCK = SFalse (%==) SCJ SCL = SFalse (%==) SCJ SCM = SFalse (%==) SCJ SCN = SFalse (%==) SCJ SCO = SFalse (%==) SCJ SCP = SFalse (%==) SCJ SCQ = SFalse (%==) SCJ SCR = SFalse (%==) SCJ SCS = SFalse (%==) SCJ SCT = SFalse (%==) SCJ SCU = SFalse (%==) SCJ SCV = SFalse (%==) SCJ SCW = SFalse (%==) SCJ SCX = SFalse (%==) SCJ SCY = SFalse (%==) SCJ SCZ = SFalse (%==) SCK SCA = SFalse (%==) SCK SCB = SFalse (%==) SCK SCC = SFalse (%==) SCK SCD = SFalse (%==) SCK SCE = SFalse (%==) SCK SCF = SFalse (%==) SCK SCG = SFalse (%==) SCK SCH = SFalse (%==) SCK SCI = SFalse (%==) SCK SCJ = SFalse (%==) SCK SCK = STrue (%==) SCK SCL = SFalse (%==) SCK SCM = SFalse (%==) SCK SCN = SFalse (%==) SCK SCO = SFalse (%==) SCK SCP = SFalse (%==) SCK SCQ = SFalse (%==) SCK SCR = SFalse (%==) SCK SCS = SFalse (%==) SCK SCT = SFalse (%==) SCK SCU = SFalse (%==) SCK SCV = SFalse (%==) SCK SCW = SFalse (%==) SCK SCX = SFalse (%==) SCK SCY = SFalse (%==) SCK SCZ = SFalse (%==) SCL SCA = SFalse (%==) SCL SCB = SFalse (%==) SCL SCC = SFalse (%==) SCL SCD = SFalse (%==) SCL SCE = SFalse (%==) SCL SCF = SFalse (%==) SCL SCG = SFalse (%==) SCL SCH = SFalse (%==) SCL SCI = SFalse (%==) SCL SCJ = SFalse (%==) SCL SCK = SFalse (%==) SCL SCL = STrue (%==) SCL SCM = SFalse (%==) SCL SCN = SFalse (%==) SCL SCO = SFalse (%==) SCL SCP = SFalse (%==) SCL SCQ = SFalse (%==) SCL SCR = SFalse (%==) SCL SCS = SFalse (%==) SCL SCT = SFalse (%==) SCL SCU = SFalse (%==) SCL SCV = SFalse (%==) SCL SCW = SFalse (%==) SCL SCX = SFalse (%==) SCL SCY = SFalse (%==) SCL SCZ = SFalse (%==) SCM SCA = SFalse (%==) SCM SCB = SFalse (%==) SCM SCC = SFalse (%==) SCM SCD = SFalse (%==) SCM SCE = SFalse (%==) SCM SCF = SFalse (%==) SCM SCG = SFalse (%==) SCM SCH = SFalse (%==) SCM SCI = SFalse (%==) SCM SCJ = SFalse (%==) SCM SCK = SFalse (%==) SCM SCL = SFalse (%==) SCM SCM = STrue (%==) SCM SCN = SFalse (%==) SCM SCO = SFalse (%==) SCM SCP = SFalse (%==) SCM SCQ = SFalse (%==) SCM SCR = SFalse (%==) SCM SCS = SFalse (%==) SCM SCT = SFalse (%==) SCM SCU = SFalse (%==) SCM SCV = SFalse (%==) SCM SCW = SFalse (%==) SCM SCX = SFalse (%==) SCM SCY = SFalse (%==) SCM SCZ = SFalse (%==) SCN SCA = SFalse (%==) SCN SCB = SFalse (%==) SCN SCC = SFalse (%==) SCN SCD = SFalse (%==) SCN SCE = SFalse (%==) SCN SCF = SFalse (%==) SCN SCG = SFalse (%==) SCN SCH = SFalse (%==) SCN SCI = SFalse (%==) SCN SCJ = SFalse (%==) SCN SCK = SFalse (%==) SCN SCL = SFalse (%==) SCN SCM = SFalse (%==) SCN SCN = STrue (%==) SCN SCO = SFalse (%==) SCN SCP = SFalse (%==) SCN SCQ = SFalse (%==) SCN SCR = SFalse (%==) SCN SCS = SFalse (%==) SCN SCT = SFalse (%==) SCN SCU = SFalse (%==) SCN SCV = SFalse (%==) SCN SCW = SFalse (%==) SCN SCX = SFalse (%==) SCN SCY = SFalse (%==) SCN SCZ = SFalse (%==) SCO SCA = SFalse (%==) SCO SCB = SFalse (%==) SCO SCC = SFalse (%==) SCO SCD = SFalse (%==) SCO SCE = SFalse (%==) SCO SCF = SFalse (%==) SCO SCG = SFalse (%==) SCO SCH = SFalse (%==) SCO SCI = SFalse (%==) SCO SCJ = SFalse (%==) SCO SCK = SFalse (%==) SCO SCL = SFalse (%==) SCO SCM = SFalse (%==) SCO SCN = SFalse (%==) SCO SCO = STrue (%==) SCO SCP = SFalse (%==) SCO SCQ = SFalse (%==) SCO SCR = SFalse (%==) SCO SCS = SFalse (%==) SCO SCT = SFalse (%==) SCO SCU = SFalse (%==) SCO SCV = SFalse (%==) SCO SCW = SFalse (%==) SCO SCX = SFalse (%==) SCO SCY = SFalse (%==) SCO SCZ = SFalse (%==) SCP SCA = SFalse (%==) SCP SCB = SFalse (%==) SCP SCC = SFalse (%==) SCP SCD = SFalse (%==) SCP SCE = SFalse (%==) SCP SCF = SFalse (%==) SCP SCG = SFalse (%==) SCP SCH = SFalse (%==) SCP SCI = SFalse (%==) SCP SCJ = SFalse (%==) SCP SCK = SFalse (%==) SCP SCL = SFalse (%==) SCP SCM = SFalse (%==) SCP SCN = SFalse (%==) SCP SCO = SFalse (%==) SCP SCP = STrue (%==) SCP SCQ = SFalse (%==) SCP SCR = SFalse (%==) SCP SCS = SFalse (%==) SCP SCT = SFalse (%==) SCP SCU = SFalse (%==) SCP SCV = SFalse (%==) SCP SCW = SFalse (%==) SCP SCX = SFalse (%==) SCP SCY = SFalse (%==) SCP SCZ = SFalse (%==) SCQ SCA = SFalse (%==) SCQ SCB = SFalse (%==) SCQ SCC = SFalse (%==) SCQ SCD = SFalse (%==) SCQ SCE = SFalse (%==) SCQ SCF = SFalse (%==) SCQ SCG = SFalse (%==) SCQ SCH = SFalse (%==) SCQ SCI = SFalse (%==) SCQ SCJ = SFalse (%==) SCQ SCK = SFalse (%==) SCQ SCL = SFalse (%==) SCQ SCM = SFalse (%==) SCQ SCN = SFalse (%==) SCQ SCO = SFalse (%==) SCQ SCP = SFalse (%==) SCQ SCQ = STrue (%==) SCQ SCR = SFalse (%==) SCQ SCS = SFalse (%==) SCQ SCT = SFalse (%==) SCQ SCU = SFalse (%==) SCQ SCV = SFalse (%==) SCQ SCW = SFalse (%==) SCQ SCX = SFalse (%==) SCQ SCY = SFalse (%==) SCQ SCZ = SFalse (%==) SCR SCA = SFalse (%==) SCR SCB = SFalse (%==) SCR SCC = SFalse (%==) SCR SCD = SFalse (%==) SCR SCE = SFalse (%==) SCR SCF = SFalse (%==) SCR SCG = SFalse (%==) SCR SCH = SFalse (%==) SCR SCI = SFalse (%==) SCR SCJ = SFalse (%==) SCR SCK = SFalse (%==) SCR SCL = SFalse (%==) SCR SCM = SFalse (%==) SCR SCN = SFalse (%==) SCR SCO = SFalse (%==) SCR SCP = SFalse (%==) SCR SCQ = SFalse (%==) SCR SCR = STrue (%==) SCR SCS = SFalse (%==) SCR SCT = SFalse (%==) SCR SCU = SFalse (%==) SCR SCV = SFalse (%==) SCR SCW = SFalse (%==) SCR SCX = SFalse (%==) SCR SCY = SFalse (%==) SCR SCZ = SFalse (%==) SCS SCA = SFalse (%==) SCS SCB = SFalse (%==) SCS SCC = SFalse (%==) SCS SCD = SFalse (%==) SCS SCE = SFalse (%==) SCS SCF = SFalse (%==) SCS SCG = SFalse (%==) SCS SCH = SFalse (%==) SCS SCI = SFalse (%==) SCS SCJ = SFalse (%==) SCS SCK = SFalse (%==) SCS SCL = SFalse (%==) SCS SCM = SFalse (%==) SCS SCN = SFalse (%==) SCS SCO = SFalse (%==) SCS SCP = SFalse (%==) SCS SCQ = SFalse (%==) SCS SCR = SFalse (%==) SCS SCS = STrue (%==) SCS SCT = SFalse (%==) SCS SCU = SFalse (%==) SCS SCV = SFalse (%==) SCS SCW = SFalse (%==) SCS SCX = SFalse (%==) SCS SCY = SFalse (%==) SCS SCZ = SFalse (%==) SCT SCA = SFalse (%==) SCT SCB = SFalse (%==) SCT SCC = SFalse (%==) SCT SCD = SFalse (%==) SCT SCE = SFalse (%==) SCT SCF = SFalse (%==) SCT SCG = SFalse (%==) SCT SCH = SFalse (%==) SCT SCI = SFalse (%==) SCT SCJ = SFalse (%==) SCT SCK = SFalse (%==) SCT SCL = SFalse (%==) SCT SCM = SFalse (%==) SCT SCN = SFalse (%==) SCT SCO = SFalse (%==) SCT SCP = SFalse (%==) SCT SCQ = SFalse (%==) SCT SCR = SFalse (%==) SCT SCS = SFalse (%==) SCT SCT = STrue (%==) SCT SCU = SFalse (%==) SCT SCV = SFalse (%==) SCT SCW = SFalse (%==) SCT SCX = SFalse (%==) SCT SCY = SFalse (%==) SCT SCZ = SFalse (%==) SCU SCA = SFalse (%==) SCU SCB = SFalse (%==) SCU SCC = SFalse (%==) SCU SCD = SFalse (%==) SCU SCE = SFalse (%==) SCU SCF = SFalse (%==) SCU SCG = SFalse (%==) SCU SCH = SFalse (%==) SCU SCI = SFalse (%==) SCU SCJ = SFalse (%==) SCU SCK = SFalse (%==) SCU SCL = SFalse (%==) SCU SCM = SFalse (%==) SCU SCN = SFalse (%==) SCU SCO = SFalse (%==) SCU SCP = SFalse (%==) SCU SCQ = SFalse (%==) SCU SCR = SFalse (%==) SCU SCS = SFalse (%==) SCU SCT = SFalse (%==) SCU SCU = STrue (%==) SCU SCV = SFalse (%==) SCU SCW = SFalse (%==) SCU SCX = SFalse (%==) SCU SCY = SFalse (%==) SCU SCZ = SFalse (%==) SCV SCA = SFalse (%==) SCV SCB = SFalse (%==) SCV SCC = SFalse (%==) SCV SCD = SFalse (%==) SCV SCE = SFalse (%==) SCV SCF = SFalse (%==) SCV SCG = SFalse (%==) SCV SCH = SFalse (%==) SCV SCI = SFalse (%==) SCV SCJ = SFalse (%==) SCV SCK = SFalse (%==) SCV SCL = SFalse (%==) SCV SCM = SFalse (%==) SCV SCN = SFalse (%==) SCV SCO = SFalse (%==) SCV SCP = SFalse (%==) SCV SCQ = SFalse (%==) SCV SCR = SFalse (%==) SCV SCS = SFalse (%==) SCV SCT = SFalse (%==) SCV SCU = SFalse (%==) SCV SCV = STrue (%==) SCV SCW = SFalse (%==) SCV SCX = SFalse (%==) SCV SCY = SFalse (%==) SCV SCZ = SFalse (%==) SCW SCA = SFalse (%==) SCW SCB = SFalse (%==) SCW SCC = SFalse (%==) SCW SCD = SFalse (%==) SCW SCE = SFalse (%==) SCW SCF = SFalse (%==) SCW SCG = SFalse (%==) SCW SCH = SFalse (%==) SCW SCI = SFalse (%==) SCW SCJ = SFalse (%==) SCW SCK = SFalse (%==) SCW SCL = SFalse (%==) SCW SCM = SFalse (%==) SCW SCN = SFalse (%==) SCW SCO = SFalse (%==) SCW SCP = SFalse (%==) SCW SCQ = SFalse (%==) SCW SCR = SFalse (%==) SCW SCS = SFalse (%==) SCW SCT = SFalse (%==) SCW SCU = SFalse (%==) SCW SCV = SFalse (%==) SCW SCW = STrue (%==) SCW SCX = SFalse (%==) SCW SCY = SFalse (%==) SCW SCZ = SFalse (%==) SCX SCA = SFalse (%==) SCX SCB = SFalse (%==) SCX SCC = SFalse (%==) SCX SCD = SFalse (%==) SCX SCE = SFalse (%==) SCX SCF = SFalse (%==) SCX SCG = SFalse (%==) SCX SCH = SFalse (%==) SCX SCI = SFalse (%==) SCX SCJ = SFalse (%==) SCX SCK = SFalse (%==) SCX SCL = SFalse (%==) SCX SCM = SFalse (%==) SCX SCN = SFalse (%==) SCX SCO = SFalse (%==) SCX SCP = SFalse (%==) SCX SCQ = SFalse (%==) SCX SCR = SFalse (%==) SCX SCS = SFalse (%==) SCX SCT = SFalse (%==) SCX SCU = SFalse (%==) SCX SCV = SFalse (%==) SCX SCW = SFalse (%==) SCX SCX = STrue (%==) SCX SCY = SFalse (%==) SCX SCZ = SFalse (%==) SCY SCA = SFalse (%==) SCY SCB = SFalse (%==) SCY SCC = SFalse (%==) SCY SCD = SFalse (%==) SCY SCE = SFalse (%==) SCY SCF = SFalse (%==) SCY SCG = SFalse (%==) SCY SCH = SFalse (%==) SCY SCI = SFalse (%==) SCY SCJ = SFalse (%==) SCY SCK = SFalse (%==) SCY SCL = SFalse (%==) SCY SCM = SFalse (%==) SCY SCN = SFalse (%==) SCY SCO = SFalse (%==) SCY SCP = SFalse (%==) SCY SCQ = SFalse (%==) SCY SCR = SFalse (%==) SCY SCS = SFalse (%==) SCY SCT = SFalse (%==) SCY SCU = SFalse (%==) SCY SCV = SFalse (%==) SCY SCW = SFalse (%==) SCY SCX = SFalse (%==) SCY SCY = STrue (%==) SCY SCZ = SFalse (%==) SCZ SCA = SFalse (%==) SCZ SCB = SFalse (%==) SCZ SCC = SFalse (%==) SCZ SCD = SFalse (%==) SCZ SCE = SFalse (%==) SCZ SCF = SFalse (%==) SCZ SCG = SFalse (%==) SCZ SCH = SFalse (%==) SCZ SCI = SFalse (%==) SCZ SCJ = SFalse (%==) SCZ SCK = SFalse (%==) SCZ SCL = SFalse (%==) SCZ SCM = SFalse (%==) SCZ SCN = SFalse (%==) SCZ SCO = SFalse (%==) SCZ SCP = SFalse (%==) SCZ SCQ = SFalse (%==) SCZ SCR = SFalse (%==) SCZ SCS = SFalse (%==) SCZ SCT = SFalse (%==) SCZ SCU = SFalse (%==) SCZ SCV = SFalse (%==) SCZ SCW = SFalse (%==) SCZ SCX = SFalse (%==) SCZ SCY = SFalse (%==) SCZ SCZ = STrue instance (SDecide U, SDecide Nat) => SDecide U where (%~) SBOOL SBOOL = Proved Refl (%~) SBOOL SSTRING = Disproved (\ x -> case x of) (%~) SBOOL SNAT = Disproved (\ x -> case x of) (%~) SBOOL (SVEC _ _) = Disproved (\ x -> case x of) (%~) SSTRING SBOOL = Disproved (\ x -> case x of) (%~) SSTRING SSTRING = Proved Refl (%~) SSTRING SNAT = Disproved (\ x -> case x of) (%~) SSTRING (SVEC _ _) = Disproved (\ x -> case x of) (%~) SNAT SBOOL = Disproved (\ x -> case x of) (%~) SNAT SSTRING = Disproved (\ x -> case x of) (%~) SNAT SNAT = Proved Refl (%~) SNAT (SVEC _ _) = Disproved (\ x -> case x of) (%~) (SVEC _ _) SBOOL = Disproved (\ x -> case x of) (%~) (SVEC _ _) SSTRING = Disproved (\ x -> case x of) (%~) (SVEC _ _) SNAT = Disproved (\ x -> case x of) (%~) (SVEC a a) (SVEC b b) = case ((,) (((%~) a) b)) (((%~) a) b) of (,) (Proved Refl) (Proved Refl) -> Proved Refl (,) (Disproved contra) _ -> Disproved (\ refl -> case refl of { Refl -> contra Refl }) (,) _ (Disproved contra) -> Disproved (\ refl -> case refl of { Refl -> contra Refl }) instance (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 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 deriving instance (Data.Singletons.ShowSing.ShowSing U, Data.Singletons.ShowSing.ShowSing Nat) => Show (SU (z :: U)) deriving instance Show (SAChar (z :: AChar)) instance SingI BOOL where sing = SBOOL instance SingI STRING where sing = SSTRING instance SingI NAT where sing = SNAT instance (SingI n, SingI n) => SingI (VEC (n :: U) (n :: Nat)) where sing = (SVEC sing) sing instance SingI (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