singletons-1.0: tests/compile-and-dump/GradingClient/Database.ghc76.template
GradingClient/Database.hs:0:0: Splicing declarations
singletons
[d| data Nat
= Zero | Succ Nat
deriving (Eq, Ord) |]
======>
GradingClient/Database.hs:(0,0)-(0,0)
data Nat
= Zero | Succ Nat
deriving (Eq, Ord)
type instance (:==) Zero Zero = TrueSym0
type instance (:==) Zero (Succ b) = FalseSym0
type instance (:==) (Succ a) Zero = FalseSym0
type instance (:==) (Succ a) (Succ b) = :== a b
type NatTyCtor = Nat
type NatTyCtorSym0 = NatTyCtor
type ZeroSym0 = Zero
data SuccSym0 (k :: TyFun Nat Nat)
type instance Apply SuccSym0 a = Succ a
data instance Sing (z :: Nat)
= z ~ Zero => SZero |
forall (n :: Nat). z ~ Succ n => SSucc (Sing n)
type SNat (z :: Nat) = Sing z
instance SingKind (KProxy :: KProxy Nat) where
type instance DemoteRep (KProxy :: KProxy Nat) = Nat
fromSing SZero = Zero
fromSing (SSucc b) = Succ (fromSing b)
toSing Zero = SomeSing SZero
toSing (Succ b)
= case toSing b :: SomeSing (KProxy :: KProxy Nat) of {
SomeSing c -> SomeSing (SSucc c) }
instance SEq (KProxy :: KProxy Nat) where
%:== SZero SZero = STrue
%:== SZero (SSucc _) = SFalse
%:== (SSucc _) SZero = SFalse
%:== (SSucc a) (SSucc b) = (%:==) a b
instance SDecide (KProxy :: KProxy Nat) where
%~ SZero SZero = Proved Refl
%~ SZero (SSucc _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SSucc _) SZero
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SSucc a) (SSucc b)
= case (%~) a b of {
Proved Refl -> Proved Refl
Disproved contra -> Disproved (\ Refl -> contra Refl) }
instance SingI Zero where
sing = SZero
instance SingI n => SingI (Succ (n :: Nat)) where
sing = SSucc sing
GradingClient/Database.hs: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] |]
======>
GradingClient/Database.hs:(0,0)-(0,0)
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 GHC.Types.[]) = True
attrNotIn (Attr name u) (Sch ((Attr name' _) GHC.Types.: t))
= ((name /= name') && (attrNotIn (Attr name u) (Sch t)))
disjoint :: Schema -> Schema -> Bool
disjoint (Sch GHC.Types.[]) _ = True
disjoint (Sch (h GHC.Types.: t)) s
= ((attrNotIn h s) && (disjoint (Sch t) s))
occurs :: [AChar] -> Schema -> Bool
occurs _ (Sch GHC.Types.[]) = False
occurs name (Sch ((Attr name' _) GHC.Types.: attrs))
= ((name == name') || (occurs name (Sch attrs)))
lookup :: [AChar] -> Schema -> U
lookup _ (Sch GHC.Types.[]) = undefined
lookup name (Sch ((Attr name' u) GHC.Types.: attrs))
= if (name == name') then u else lookup name (Sch attrs)
type instance (:==) BOOL BOOL = TrueSym0
type instance (:==) BOOL STRING = FalseSym0
type instance (:==) BOOL NAT = FalseSym0
type instance (:==) BOOL (VEC b b) = FalseSym0
type instance (:==) STRING BOOL = FalseSym0
type instance (:==) STRING STRING = TrueSym0
type instance (:==) STRING NAT = FalseSym0
type instance (:==) STRING (VEC b b) = FalseSym0
type instance (:==) NAT BOOL = FalseSym0
type instance (:==) NAT STRING = FalseSym0
type instance (:==) NAT NAT = TrueSym0
type instance (:==) NAT (VEC b b) = FalseSym0
type instance (:==) (VEC a a) BOOL = FalseSym0
type instance (:==) (VEC a a) STRING = FalseSym0
type instance (:==) (VEC a a) NAT = FalseSym0
type instance (:==) (VEC a a) (VEC b b) = :&& (:== a b) (:== a b)
type UTyCtor = U
type UTyCtorSym0 = UTyCtor
type BOOLSym0 = BOOL
type STRINGSym0 = STRING
type NATSym0 = NAT
data VECSym1 (l :: U) (l :: TyFun Nat U)
data VECSym0 (k :: TyFun U (TyFun Nat U -> *))
type instance Apply (VECSym1 a) a = VEC a a
type instance Apply VECSym0 a = VECSym1 a
type instance (:==) CA CA = TrueSym0
type instance (:==) CA CB = FalseSym0
type instance (:==) CA CC = FalseSym0
type instance (:==) CA CD = FalseSym0
type instance (:==) CA CE = FalseSym0
type instance (:==) CA CF = FalseSym0
type instance (:==) CA CG = FalseSym0
type instance (:==) CA CH = FalseSym0
type instance (:==) CA CI = FalseSym0
type instance (:==) CA CJ = FalseSym0
type instance (:==) CA CK = FalseSym0
type instance (:==) CA CL = FalseSym0
type instance (:==) CA CM = FalseSym0
type instance (:==) CA CN = FalseSym0
type instance (:==) CA CO = FalseSym0
type instance (:==) CA CP = FalseSym0
type instance (:==) CA CQ = FalseSym0
type instance (:==) CA CR = FalseSym0
type instance (:==) CA CS = FalseSym0
type instance (:==) CA CT = FalseSym0
type instance (:==) CA CU = FalseSym0
type instance (:==) CA CV = FalseSym0
type instance (:==) CA CW = FalseSym0
type instance (:==) CA CX = FalseSym0
type instance (:==) CA CY = FalseSym0
type instance (:==) CA CZ = FalseSym0
type instance (:==) CB CA = FalseSym0
type instance (:==) CB CB = TrueSym0
type instance (:==) CB CC = FalseSym0
type instance (:==) CB CD = FalseSym0
type instance (:==) CB CE = FalseSym0
type instance (:==) CB CF = FalseSym0
type instance (:==) CB CG = FalseSym0
type instance (:==) CB CH = FalseSym0
type instance (:==) CB CI = FalseSym0
type instance (:==) CB CJ = FalseSym0
type instance (:==) CB CK = FalseSym0
type instance (:==) CB CL = FalseSym0
type instance (:==) CB CM = FalseSym0
type instance (:==) CB CN = FalseSym0
type instance (:==) CB CO = FalseSym0
type instance (:==) CB CP = FalseSym0
type instance (:==) CB CQ = FalseSym0
type instance (:==) CB CR = FalseSym0
type instance (:==) CB CS = FalseSym0
type instance (:==) CB CT = FalseSym0
type instance (:==) CB CU = FalseSym0
type instance (:==) CB CV = FalseSym0
type instance (:==) CB CW = FalseSym0
type instance (:==) CB CX = FalseSym0
type instance (:==) CB CY = FalseSym0
type instance (:==) CB CZ = FalseSym0
type instance (:==) CC CA = FalseSym0
type instance (:==) CC CB = FalseSym0
type instance (:==) CC CC = TrueSym0
type instance (:==) CC CD = FalseSym0
type instance (:==) CC CE = FalseSym0
type instance (:==) CC CF = FalseSym0
type instance (:==) CC CG = FalseSym0
type instance (:==) CC CH = FalseSym0
type instance (:==) CC CI = FalseSym0
type instance (:==) CC CJ = FalseSym0
type instance (:==) CC CK = FalseSym0
type instance (:==) CC CL = FalseSym0
type instance (:==) CC CM = FalseSym0
type instance (:==) CC CN = FalseSym0
type instance (:==) CC CO = FalseSym0
type instance (:==) CC CP = FalseSym0
type instance (:==) CC CQ = FalseSym0
type instance (:==) CC CR = FalseSym0
type instance (:==) CC CS = FalseSym0
type instance (:==) CC CT = FalseSym0
type instance (:==) CC CU = FalseSym0
type instance (:==) CC CV = FalseSym0
type instance (:==) CC CW = FalseSym0
type instance (:==) CC CX = FalseSym0
type instance (:==) CC CY = FalseSym0
type instance (:==) CC CZ = FalseSym0
type instance (:==) CD CA = FalseSym0
type instance (:==) CD CB = FalseSym0
type instance (:==) CD CC = FalseSym0
type instance (:==) CD CD = TrueSym0
type instance (:==) CD CE = FalseSym0
type instance (:==) CD CF = FalseSym0
type instance (:==) CD CG = FalseSym0
type instance (:==) CD CH = FalseSym0
type instance (:==) CD CI = FalseSym0
type instance (:==) CD CJ = FalseSym0
type instance (:==) CD CK = FalseSym0
type instance (:==) CD CL = FalseSym0
type instance (:==) CD CM = FalseSym0
type instance (:==) CD CN = FalseSym0
type instance (:==) CD CO = FalseSym0
type instance (:==) CD CP = FalseSym0
type instance (:==) CD CQ = FalseSym0
type instance (:==) CD CR = FalseSym0
type instance (:==) CD CS = FalseSym0
type instance (:==) CD CT = FalseSym0
type instance (:==) CD CU = FalseSym0
type instance (:==) CD CV = FalseSym0
type instance (:==) CD CW = FalseSym0
type instance (:==) CD CX = FalseSym0
type instance (:==) CD CY = FalseSym0
type instance (:==) CD CZ = FalseSym0
type instance (:==) CE CA = FalseSym0
type instance (:==) CE CB = FalseSym0
type instance (:==) CE CC = FalseSym0
type instance (:==) CE CD = FalseSym0
type instance (:==) CE CE = TrueSym0
type instance (:==) CE CF = FalseSym0
type instance (:==) CE CG = FalseSym0
type instance (:==) CE CH = FalseSym0
type instance (:==) CE CI = FalseSym0
type instance (:==) CE CJ = FalseSym0
type instance (:==) CE CK = FalseSym0
type instance (:==) CE CL = FalseSym0
type instance (:==) CE CM = FalseSym0
type instance (:==) CE CN = FalseSym0
type instance (:==) CE CO = FalseSym0
type instance (:==) CE CP = FalseSym0
type instance (:==) CE CQ = FalseSym0
type instance (:==) CE CR = FalseSym0
type instance (:==) CE CS = FalseSym0
type instance (:==) CE CT = FalseSym0
type instance (:==) CE CU = FalseSym0
type instance (:==) CE CV = FalseSym0
type instance (:==) CE CW = FalseSym0
type instance (:==) CE CX = FalseSym0
type instance (:==) CE CY = FalseSym0
type instance (:==) CE CZ = FalseSym0
type instance (:==) CF CA = FalseSym0
type instance (:==) CF CB = FalseSym0
type instance (:==) CF CC = FalseSym0
type instance (:==) CF CD = FalseSym0
type instance (:==) CF CE = FalseSym0
type instance (:==) CF CF = TrueSym0
type instance (:==) CF CG = FalseSym0
type instance (:==) CF CH = FalseSym0
type instance (:==) CF CI = FalseSym0
type instance (:==) CF CJ = FalseSym0
type instance (:==) CF CK = FalseSym0
type instance (:==) CF CL = FalseSym0
type instance (:==) CF CM = FalseSym0
type instance (:==) CF CN = FalseSym0
type instance (:==) CF CO = FalseSym0
type instance (:==) CF CP = FalseSym0
type instance (:==) CF CQ = FalseSym0
type instance (:==) CF CR = FalseSym0
type instance (:==) CF CS = FalseSym0
type instance (:==) CF CT = FalseSym0
type instance (:==) CF CU = FalseSym0
type instance (:==) CF CV = FalseSym0
type instance (:==) CF CW = FalseSym0
type instance (:==) CF CX = FalseSym0
type instance (:==) CF CY = FalseSym0
type instance (:==) CF CZ = FalseSym0
type instance (:==) CG CA = FalseSym0
type instance (:==) CG CB = FalseSym0
type instance (:==) CG CC = FalseSym0
type instance (:==) CG CD = FalseSym0
type instance (:==) CG CE = FalseSym0
type instance (:==) CG CF = FalseSym0
type instance (:==) CG CG = TrueSym0
type instance (:==) CG CH = FalseSym0
type instance (:==) CG CI = FalseSym0
type instance (:==) CG CJ = FalseSym0
type instance (:==) CG CK = FalseSym0
type instance (:==) CG CL = FalseSym0
type instance (:==) CG CM = FalseSym0
type instance (:==) CG CN = FalseSym0
type instance (:==) CG CO = FalseSym0
type instance (:==) CG CP = FalseSym0
type instance (:==) CG CQ = FalseSym0
type instance (:==) CG CR = FalseSym0
type instance (:==) CG CS = FalseSym0
type instance (:==) CG CT = FalseSym0
type instance (:==) CG CU = FalseSym0
type instance (:==) CG CV = FalseSym0
type instance (:==) CG CW = FalseSym0
type instance (:==) CG CX = FalseSym0
type instance (:==) CG CY = FalseSym0
type instance (:==) CG CZ = FalseSym0
type instance (:==) CH CA = FalseSym0
type instance (:==) CH CB = FalseSym0
type instance (:==) CH CC = FalseSym0
type instance (:==) CH CD = FalseSym0
type instance (:==) CH CE = FalseSym0
type instance (:==) CH CF = FalseSym0
type instance (:==) CH CG = FalseSym0
type instance (:==) CH CH = TrueSym0
type instance (:==) CH CI = FalseSym0
type instance (:==) CH CJ = FalseSym0
type instance (:==) CH CK = FalseSym0
type instance (:==) CH CL = FalseSym0
type instance (:==) CH CM = FalseSym0
type instance (:==) CH CN = FalseSym0
type instance (:==) CH CO = FalseSym0
type instance (:==) CH CP = FalseSym0
type instance (:==) CH CQ = FalseSym0
type instance (:==) CH CR = FalseSym0
type instance (:==) CH CS = FalseSym0
type instance (:==) CH CT = FalseSym0
type instance (:==) CH CU = FalseSym0
type instance (:==) CH CV = FalseSym0
type instance (:==) CH CW = FalseSym0
type instance (:==) CH CX = FalseSym0
type instance (:==) CH CY = FalseSym0
type instance (:==) CH CZ = FalseSym0
type instance (:==) CI CA = FalseSym0
type instance (:==) CI CB = FalseSym0
type instance (:==) CI CC = FalseSym0
type instance (:==) CI CD = FalseSym0
type instance (:==) CI CE = FalseSym0
type instance (:==) CI CF = FalseSym0
type instance (:==) CI CG = FalseSym0
type instance (:==) CI CH = FalseSym0
type instance (:==) CI CI = TrueSym0
type instance (:==) CI CJ = FalseSym0
type instance (:==) CI CK = FalseSym0
type instance (:==) CI CL = FalseSym0
type instance (:==) CI CM = FalseSym0
type instance (:==) CI CN = FalseSym0
type instance (:==) CI CO = FalseSym0
type instance (:==) CI CP = FalseSym0
type instance (:==) CI CQ = FalseSym0
type instance (:==) CI CR = FalseSym0
type instance (:==) CI CS = FalseSym0
type instance (:==) CI CT = FalseSym0
type instance (:==) CI CU = FalseSym0
type instance (:==) CI CV = FalseSym0
type instance (:==) CI CW = FalseSym0
type instance (:==) CI CX = FalseSym0
type instance (:==) CI CY = FalseSym0
type instance (:==) CI CZ = FalseSym0
type instance (:==) CJ CA = FalseSym0
type instance (:==) CJ CB = FalseSym0
type instance (:==) CJ CC = FalseSym0
type instance (:==) CJ CD = FalseSym0
type instance (:==) CJ CE = FalseSym0
type instance (:==) CJ CF = FalseSym0
type instance (:==) CJ CG = FalseSym0
type instance (:==) CJ CH = FalseSym0
type instance (:==) CJ CI = FalseSym0
type instance (:==) CJ CJ = TrueSym0
type instance (:==) CJ CK = FalseSym0
type instance (:==) CJ CL = FalseSym0
type instance (:==) CJ CM = FalseSym0
type instance (:==) CJ CN = FalseSym0
type instance (:==) CJ CO = FalseSym0
type instance (:==) CJ CP = FalseSym0
type instance (:==) CJ CQ = FalseSym0
type instance (:==) CJ CR = FalseSym0
type instance (:==) CJ CS = FalseSym0
type instance (:==) CJ CT = FalseSym0
type instance (:==) CJ CU = FalseSym0
type instance (:==) CJ CV = FalseSym0
type instance (:==) CJ CW = FalseSym0
type instance (:==) CJ CX = FalseSym0
type instance (:==) CJ CY = FalseSym0
type instance (:==) CJ CZ = FalseSym0
type instance (:==) CK CA = FalseSym0
type instance (:==) CK CB = FalseSym0
type instance (:==) CK CC = FalseSym0
type instance (:==) CK CD = FalseSym0
type instance (:==) CK CE = FalseSym0
type instance (:==) CK CF = FalseSym0
type instance (:==) CK CG = FalseSym0
type instance (:==) CK CH = FalseSym0
type instance (:==) CK CI = FalseSym0
type instance (:==) CK CJ = FalseSym0
type instance (:==) CK CK = TrueSym0
type instance (:==) CK CL = FalseSym0
type instance (:==) CK CM = FalseSym0
type instance (:==) CK CN = FalseSym0
type instance (:==) CK CO = FalseSym0
type instance (:==) CK CP = FalseSym0
type instance (:==) CK CQ = FalseSym0
type instance (:==) CK CR = FalseSym0
type instance (:==) CK CS = FalseSym0
type instance (:==) CK CT = FalseSym0
type instance (:==) CK CU = FalseSym0
type instance (:==) CK CV = FalseSym0
type instance (:==) CK CW = FalseSym0
type instance (:==) CK CX = FalseSym0
type instance (:==) CK CY = FalseSym0
type instance (:==) CK CZ = FalseSym0
type instance (:==) CL CA = FalseSym0
type instance (:==) CL CB = FalseSym0
type instance (:==) CL CC = FalseSym0
type instance (:==) CL CD = FalseSym0
type instance (:==) CL CE = FalseSym0
type instance (:==) CL CF = FalseSym0
type instance (:==) CL CG = FalseSym0
type instance (:==) CL CH = FalseSym0
type instance (:==) CL CI = FalseSym0
type instance (:==) CL CJ = FalseSym0
type instance (:==) CL CK = FalseSym0
type instance (:==) CL CL = TrueSym0
type instance (:==) CL CM = FalseSym0
type instance (:==) CL CN = FalseSym0
type instance (:==) CL CO = FalseSym0
type instance (:==) CL CP = FalseSym0
type instance (:==) CL CQ = FalseSym0
type instance (:==) CL CR = FalseSym0
type instance (:==) CL CS = FalseSym0
type instance (:==) CL CT = FalseSym0
type instance (:==) CL CU = FalseSym0
type instance (:==) CL CV = FalseSym0
type instance (:==) CL CW = FalseSym0
type instance (:==) CL CX = FalseSym0
type instance (:==) CL CY = FalseSym0
type instance (:==) CL CZ = FalseSym0
type instance (:==) CM CA = FalseSym0
type instance (:==) CM CB = FalseSym0
type instance (:==) CM CC = FalseSym0
type instance (:==) CM CD = FalseSym0
type instance (:==) CM CE = FalseSym0
type instance (:==) CM CF = FalseSym0
type instance (:==) CM CG = FalseSym0
type instance (:==) CM CH = FalseSym0
type instance (:==) CM CI = FalseSym0
type instance (:==) CM CJ = FalseSym0
type instance (:==) CM CK = FalseSym0
type instance (:==) CM CL = FalseSym0
type instance (:==) CM CM = TrueSym0
type instance (:==) CM CN = FalseSym0
type instance (:==) CM CO = FalseSym0
type instance (:==) CM CP = FalseSym0
type instance (:==) CM CQ = FalseSym0
type instance (:==) CM CR = FalseSym0
type instance (:==) CM CS = FalseSym0
type instance (:==) CM CT = FalseSym0
type instance (:==) CM CU = FalseSym0
type instance (:==) CM CV = FalseSym0
type instance (:==) CM CW = FalseSym0
type instance (:==) CM CX = FalseSym0
type instance (:==) CM CY = FalseSym0
type instance (:==) CM CZ = FalseSym0
type instance (:==) CN CA = FalseSym0
type instance (:==) CN CB = FalseSym0
type instance (:==) CN CC = FalseSym0
type instance (:==) CN CD = FalseSym0
type instance (:==) CN CE = FalseSym0
type instance (:==) CN CF = FalseSym0
type instance (:==) CN CG = FalseSym0
type instance (:==) CN CH = FalseSym0
type instance (:==) CN CI = FalseSym0
type instance (:==) CN CJ = FalseSym0
type instance (:==) CN CK = FalseSym0
type instance (:==) CN CL = FalseSym0
type instance (:==) CN CM = FalseSym0
type instance (:==) CN CN = TrueSym0
type instance (:==) CN CO = FalseSym0
type instance (:==) CN CP = FalseSym0
type instance (:==) CN CQ = FalseSym0
type instance (:==) CN CR = FalseSym0
type instance (:==) CN CS = FalseSym0
type instance (:==) CN CT = FalseSym0
type instance (:==) CN CU = FalseSym0
type instance (:==) CN CV = FalseSym0
type instance (:==) CN CW = FalseSym0
type instance (:==) CN CX = FalseSym0
type instance (:==) CN CY = FalseSym0
type instance (:==) CN CZ = FalseSym0
type instance (:==) CO CA = FalseSym0
type instance (:==) CO CB = FalseSym0
type instance (:==) CO CC = FalseSym0
type instance (:==) CO CD = FalseSym0
type instance (:==) CO CE = FalseSym0
type instance (:==) CO CF = FalseSym0
type instance (:==) CO CG = FalseSym0
type instance (:==) CO CH = FalseSym0
type instance (:==) CO CI = FalseSym0
type instance (:==) CO CJ = FalseSym0
type instance (:==) CO CK = FalseSym0
type instance (:==) CO CL = FalseSym0
type instance (:==) CO CM = FalseSym0
type instance (:==) CO CN = FalseSym0
type instance (:==) CO CO = TrueSym0
type instance (:==) CO CP = FalseSym0
type instance (:==) CO CQ = FalseSym0
type instance (:==) CO CR = FalseSym0
type instance (:==) CO CS = FalseSym0
type instance (:==) CO CT = FalseSym0
type instance (:==) CO CU = FalseSym0
type instance (:==) CO CV = FalseSym0
type instance (:==) CO CW = FalseSym0
type instance (:==) CO CX = FalseSym0
type instance (:==) CO CY = FalseSym0
type instance (:==) CO CZ = FalseSym0
type instance (:==) CP CA = FalseSym0
type instance (:==) CP CB = FalseSym0
type instance (:==) CP CC = FalseSym0
type instance (:==) CP CD = FalseSym0
type instance (:==) CP CE = FalseSym0
type instance (:==) CP CF = FalseSym0
type instance (:==) CP CG = FalseSym0
type instance (:==) CP CH = FalseSym0
type instance (:==) CP CI = FalseSym0
type instance (:==) CP CJ = FalseSym0
type instance (:==) CP CK = FalseSym0
type instance (:==) CP CL = FalseSym0
type instance (:==) CP CM = FalseSym0
type instance (:==) CP CN = FalseSym0
type instance (:==) CP CO = FalseSym0
type instance (:==) CP CP = TrueSym0
type instance (:==) CP CQ = FalseSym0
type instance (:==) CP CR = FalseSym0
type instance (:==) CP CS = FalseSym0
type instance (:==) CP CT = FalseSym0
type instance (:==) CP CU = FalseSym0
type instance (:==) CP CV = FalseSym0
type instance (:==) CP CW = FalseSym0
type instance (:==) CP CX = FalseSym0
type instance (:==) CP CY = FalseSym0
type instance (:==) CP CZ = FalseSym0
type instance (:==) CQ CA = FalseSym0
type instance (:==) CQ CB = FalseSym0
type instance (:==) CQ CC = FalseSym0
type instance (:==) CQ CD = FalseSym0
type instance (:==) CQ CE = FalseSym0
type instance (:==) CQ CF = FalseSym0
type instance (:==) CQ CG = FalseSym0
type instance (:==) CQ CH = FalseSym0
type instance (:==) CQ CI = FalseSym0
type instance (:==) CQ CJ = FalseSym0
type instance (:==) CQ CK = FalseSym0
type instance (:==) CQ CL = FalseSym0
type instance (:==) CQ CM = FalseSym0
type instance (:==) CQ CN = FalseSym0
type instance (:==) CQ CO = FalseSym0
type instance (:==) CQ CP = FalseSym0
type instance (:==) CQ CQ = TrueSym0
type instance (:==) CQ CR = FalseSym0
type instance (:==) CQ CS = FalseSym0
type instance (:==) CQ CT = FalseSym0
type instance (:==) CQ CU = FalseSym0
type instance (:==) CQ CV = FalseSym0
type instance (:==) CQ CW = FalseSym0
type instance (:==) CQ CX = FalseSym0
type instance (:==) CQ CY = FalseSym0
type instance (:==) CQ CZ = FalseSym0
type instance (:==) CR CA = FalseSym0
type instance (:==) CR CB = FalseSym0
type instance (:==) CR CC = FalseSym0
type instance (:==) CR CD = FalseSym0
type instance (:==) CR CE = FalseSym0
type instance (:==) CR CF = FalseSym0
type instance (:==) CR CG = FalseSym0
type instance (:==) CR CH = FalseSym0
type instance (:==) CR CI = FalseSym0
type instance (:==) CR CJ = FalseSym0
type instance (:==) CR CK = FalseSym0
type instance (:==) CR CL = FalseSym0
type instance (:==) CR CM = FalseSym0
type instance (:==) CR CN = FalseSym0
type instance (:==) CR CO = FalseSym0
type instance (:==) CR CP = FalseSym0
type instance (:==) CR CQ = FalseSym0
type instance (:==) CR CR = TrueSym0
type instance (:==) CR CS = FalseSym0
type instance (:==) CR CT = FalseSym0
type instance (:==) CR CU = FalseSym0
type instance (:==) CR CV = FalseSym0
type instance (:==) CR CW = FalseSym0
type instance (:==) CR CX = FalseSym0
type instance (:==) CR CY = FalseSym0
type instance (:==) CR CZ = FalseSym0
type instance (:==) CS CA = FalseSym0
type instance (:==) CS CB = FalseSym0
type instance (:==) CS CC = FalseSym0
type instance (:==) CS CD = FalseSym0
type instance (:==) CS CE = FalseSym0
type instance (:==) CS CF = FalseSym0
type instance (:==) CS CG = FalseSym0
type instance (:==) CS CH = FalseSym0
type instance (:==) CS CI = FalseSym0
type instance (:==) CS CJ = FalseSym0
type instance (:==) CS CK = FalseSym0
type instance (:==) CS CL = FalseSym0
type instance (:==) CS CM = FalseSym0
type instance (:==) CS CN = FalseSym0
type instance (:==) CS CO = FalseSym0
type instance (:==) CS CP = FalseSym0
type instance (:==) CS CQ = FalseSym0
type instance (:==) CS CR = FalseSym0
type instance (:==) CS CS = TrueSym0
type instance (:==) CS CT = FalseSym0
type instance (:==) CS CU = FalseSym0
type instance (:==) CS CV = FalseSym0
type instance (:==) CS CW = FalseSym0
type instance (:==) CS CX = FalseSym0
type instance (:==) CS CY = FalseSym0
type instance (:==) CS CZ = FalseSym0
type instance (:==) CT CA = FalseSym0
type instance (:==) CT CB = FalseSym0
type instance (:==) CT CC = FalseSym0
type instance (:==) CT CD = FalseSym0
type instance (:==) CT CE = FalseSym0
type instance (:==) CT CF = FalseSym0
type instance (:==) CT CG = FalseSym0
type instance (:==) CT CH = FalseSym0
type instance (:==) CT CI = FalseSym0
type instance (:==) CT CJ = FalseSym0
type instance (:==) CT CK = FalseSym0
type instance (:==) CT CL = FalseSym0
type instance (:==) CT CM = FalseSym0
type instance (:==) CT CN = FalseSym0
type instance (:==) CT CO = FalseSym0
type instance (:==) CT CP = FalseSym0
type instance (:==) CT CQ = FalseSym0
type instance (:==) CT CR = FalseSym0
type instance (:==) CT CS = FalseSym0
type instance (:==) CT CT = TrueSym0
type instance (:==) CT CU = FalseSym0
type instance (:==) CT CV = FalseSym0
type instance (:==) CT CW = FalseSym0
type instance (:==) CT CX = FalseSym0
type instance (:==) CT CY = FalseSym0
type instance (:==) CT CZ = FalseSym0
type instance (:==) CU CA = FalseSym0
type instance (:==) CU CB = FalseSym0
type instance (:==) CU CC = FalseSym0
type instance (:==) CU CD = FalseSym0
type instance (:==) CU CE = FalseSym0
type instance (:==) CU CF = FalseSym0
type instance (:==) CU CG = FalseSym0
type instance (:==) CU CH = FalseSym0
type instance (:==) CU CI = FalseSym0
type instance (:==) CU CJ = FalseSym0
type instance (:==) CU CK = FalseSym0
type instance (:==) CU CL = FalseSym0
type instance (:==) CU CM = FalseSym0
type instance (:==) CU CN = FalseSym0
type instance (:==) CU CO = FalseSym0
type instance (:==) CU CP = FalseSym0
type instance (:==) CU CQ = FalseSym0
type instance (:==) CU CR = FalseSym0
type instance (:==) CU CS = FalseSym0
type instance (:==) CU CT = FalseSym0
type instance (:==) CU CU = TrueSym0
type instance (:==) CU CV = FalseSym0
type instance (:==) CU CW = FalseSym0
type instance (:==) CU CX = FalseSym0
type instance (:==) CU CY = FalseSym0
type instance (:==) CU CZ = FalseSym0
type instance (:==) CV CA = FalseSym0
type instance (:==) CV CB = FalseSym0
type instance (:==) CV CC = FalseSym0
type instance (:==) CV CD = FalseSym0
type instance (:==) CV CE = FalseSym0
type instance (:==) CV CF = FalseSym0
type instance (:==) CV CG = FalseSym0
type instance (:==) CV CH = FalseSym0
type instance (:==) CV CI = FalseSym0
type instance (:==) CV CJ = FalseSym0
type instance (:==) CV CK = FalseSym0
type instance (:==) CV CL = FalseSym0
type instance (:==) CV CM = FalseSym0
type instance (:==) CV CN = FalseSym0
type instance (:==) CV CO = FalseSym0
type instance (:==) CV CP = FalseSym0
type instance (:==) CV CQ = FalseSym0
type instance (:==) CV CR = FalseSym0
type instance (:==) CV CS = FalseSym0
type instance (:==) CV CT = FalseSym0
type instance (:==) CV CU = FalseSym0
type instance (:==) CV CV = TrueSym0
type instance (:==) CV CW = FalseSym0
type instance (:==) CV CX = FalseSym0
type instance (:==) CV CY = FalseSym0
type instance (:==) CV CZ = FalseSym0
type instance (:==) CW CA = FalseSym0
type instance (:==) CW CB = FalseSym0
type instance (:==) CW CC = FalseSym0
type instance (:==) CW CD = FalseSym0
type instance (:==) CW CE = FalseSym0
type instance (:==) CW CF = FalseSym0
type instance (:==) CW CG = FalseSym0
type instance (:==) CW CH = FalseSym0
type instance (:==) CW CI = FalseSym0
type instance (:==) CW CJ = FalseSym0
type instance (:==) CW CK = FalseSym0
type instance (:==) CW CL = FalseSym0
type instance (:==) CW CM = FalseSym0
type instance (:==) CW CN = FalseSym0
type instance (:==) CW CO = FalseSym0
type instance (:==) CW CP = FalseSym0
type instance (:==) CW CQ = FalseSym0
type instance (:==) CW CR = FalseSym0
type instance (:==) CW CS = FalseSym0
type instance (:==) CW CT = FalseSym0
type instance (:==) CW CU = FalseSym0
type instance (:==) CW CV = FalseSym0
type instance (:==) CW CW = TrueSym0
type instance (:==) CW CX = FalseSym0
type instance (:==) CW CY = FalseSym0
type instance (:==) CW CZ = FalseSym0
type instance (:==) CX CA = FalseSym0
type instance (:==) CX CB = FalseSym0
type instance (:==) CX CC = FalseSym0
type instance (:==) CX CD = FalseSym0
type instance (:==) CX CE = FalseSym0
type instance (:==) CX CF = FalseSym0
type instance (:==) CX CG = FalseSym0
type instance (:==) CX CH = FalseSym0
type instance (:==) CX CI = FalseSym0
type instance (:==) CX CJ = FalseSym0
type instance (:==) CX CK = FalseSym0
type instance (:==) CX CL = FalseSym0
type instance (:==) CX CM = FalseSym0
type instance (:==) CX CN = FalseSym0
type instance (:==) CX CO = FalseSym0
type instance (:==) CX CP = FalseSym0
type instance (:==) CX CQ = FalseSym0
type instance (:==) CX CR = FalseSym0
type instance (:==) CX CS = FalseSym0
type instance (:==) CX CT = FalseSym0
type instance (:==) CX CU = FalseSym0
type instance (:==) CX CV = FalseSym0
type instance (:==) CX CW = FalseSym0
type instance (:==) CX CX = TrueSym0
type instance (:==) CX CY = FalseSym0
type instance (:==) CX CZ = FalseSym0
type instance (:==) CY CA = FalseSym0
type instance (:==) CY CB = FalseSym0
type instance (:==) CY CC = FalseSym0
type instance (:==) CY CD = FalseSym0
type instance (:==) CY CE = FalseSym0
type instance (:==) CY CF = FalseSym0
type instance (:==) CY CG = FalseSym0
type instance (:==) CY CH = FalseSym0
type instance (:==) CY CI = FalseSym0
type instance (:==) CY CJ = FalseSym0
type instance (:==) CY CK = FalseSym0
type instance (:==) CY CL = FalseSym0
type instance (:==) CY CM = FalseSym0
type instance (:==) CY CN = FalseSym0
type instance (:==) CY CO = FalseSym0
type instance (:==) CY CP = FalseSym0
type instance (:==) CY CQ = FalseSym0
type instance (:==) CY CR = FalseSym0
type instance (:==) CY CS = FalseSym0
type instance (:==) CY CT = FalseSym0
type instance (:==) CY CU = FalseSym0
type instance (:==) CY CV = FalseSym0
type instance (:==) CY CW = FalseSym0
type instance (:==) CY CX = FalseSym0
type instance (:==) CY CY = TrueSym0
type instance (:==) CY CZ = FalseSym0
type instance (:==) CZ CA = FalseSym0
type instance (:==) CZ CB = FalseSym0
type instance (:==) CZ CC = FalseSym0
type instance (:==) CZ CD = FalseSym0
type instance (:==) CZ CE = FalseSym0
type instance (:==) CZ CF = FalseSym0
type instance (:==) CZ CG = FalseSym0
type instance (:==) CZ CH = FalseSym0
type instance (:==) CZ CI = FalseSym0
type instance (:==) CZ CJ = FalseSym0
type instance (:==) CZ CK = FalseSym0
type instance (:==) CZ CL = FalseSym0
type instance (:==) CZ CM = FalseSym0
type instance (:==) CZ CN = FalseSym0
type instance (:==) CZ CO = FalseSym0
type instance (:==) CZ CP = FalseSym0
type instance (:==) CZ CQ = FalseSym0
type instance (:==) CZ CR = FalseSym0
type instance (:==) CZ CS = FalseSym0
type instance (:==) CZ CT = FalseSym0
type instance (:==) CZ CU = FalseSym0
type instance (:==) CZ CV = FalseSym0
type instance (:==) CZ CW = FalseSym0
type instance (:==) CZ CX = FalseSym0
type instance (:==) CZ CY = FalseSym0
type instance (:==) CZ CZ = TrueSym0
type ACharTyCtor = AChar
type ACharTyCtorSym0 = ACharTyCtor
type CASym0 = CA
type CBSym0 = CB
type CCSym0 = CC
type CDSym0 = CD
type CESym0 = CE
type CFSym0 = CF
type CGSym0 = CG
type CHSym0 = CH
type CISym0 = CI
type CJSym0 = CJ
type CKSym0 = CK
type CLSym0 = CL
type CMSym0 = CM
type CNSym0 = CN
type COSym0 = CO
type CPSym0 = CP
type CQSym0 = CQ
type CRSym0 = CR
type CSSym0 = CS
type CTSym0 = CT
type CUSym0 = CU
type CVSym0 = CV
type CWSym0 = CW
type CXSym0 = CX
type CYSym0 = CY
type CZSym0 = CZ
type AttributeTyCtor = Attribute
type AttributeTyCtorSym0 = AttributeTyCtor
data AttrSym1 (l :: [AChar]) (l :: TyFun U Attribute)
data AttrSym0 (k :: TyFun [AChar] (TyFun U Attribute -> *))
type instance Apply (AttrSym1 a) a = Attr a a
type instance Apply AttrSym0 a = AttrSym1 a
type SchemaTyCtor = Schema
type SchemaTyCtorSym0 = SchemaTyCtor
data SchSym0 (k :: TyFun [Attribute] Schema)
type instance Apply SchSym0 a = Sch a
type family Append (a :: Schema) (a :: Schema) :: Schema
type instance Append (Sch s1) (Sch s2) =
Apply SchSym0 (Apply (Apply :++$ s1) s2)
data AppendSym1 (l :: Schema) (l :: TyFun Schema Schema)
data AppendSym0 (k :: TyFun Schema (TyFun Schema Schema -> *))
type instance Apply (AppendSym1 a) a = Append a a
type instance Apply AppendSym0 a = AppendSym1 a
type family AttrNotIn (a :: Attribute) (a :: Schema) :: Bool
type instance AttrNotIn z (Sch GHC.Types.[]) = TrueSym0
type instance AttrNotIn (Attr name u) (Sch (GHC.Types.: (Attr name' z) t)) =
Apply (Apply :&&$ (Apply (Apply :/=$ name) name')) (Apply (Apply AttrNotInSym0 (Apply (Apply AttrSym0 name) u)) (Apply SchSym0 t))
data AttrNotInSym1 (l :: Attribute) (l :: TyFun Schema Bool)
data AttrNotInSym0 (k :: TyFun Attribute (TyFun Schema Bool -> *))
type instance Apply (AttrNotInSym1 a) a = AttrNotIn a a
type instance Apply AttrNotInSym0 a = AttrNotInSym1 a
type family Disjoint (a :: Schema) (a :: Schema) :: Bool
type instance Disjoint (Sch GHC.Types.[]) z = TrueSym0
type instance Disjoint (Sch (GHC.Types.: h t)) s =
Apply (Apply :&&$ (Apply (Apply AttrNotInSym0 h) s)) (Apply (Apply DisjointSym0 (Apply SchSym0 t)) s)
data DisjointSym1 (l :: Schema) (l :: TyFun Schema Bool)
data DisjointSym0 (k :: TyFun Schema (TyFun Schema Bool -> *))
type instance Apply (DisjointSym1 a) a = Disjoint a a
type instance Apply DisjointSym0 a = DisjointSym1 a
type family Occurs (a :: [AChar]) (a :: Schema) :: Bool
type instance Occurs z (Sch GHC.Types.[]) = FalseSym0
type instance Occurs name (Sch (GHC.Types.: (Attr name' z) attrs)) =
Apply (Apply :||$ (Apply (Apply :==$ name) name')) (Apply (Apply OccursSym0 name) (Apply SchSym0 attrs))
data OccursSym1 (l :: [AChar]) (l :: TyFun Schema Bool)
data OccursSym0 (k :: TyFun [AChar] (TyFun Schema Bool -> *))
type instance Apply (OccursSym1 a) a = Occurs a a
type instance Apply OccursSym0 a = OccursSym1 a
type family Lookup (a :: [AChar]) (a :: Schema) :: U
type instance Lookup z (Sch GHC.Types.[]) = Any
type instance Lookup name (Sch (GHC.Types.: (Attr name' u) attrs)) =
If (Apply (Apply :==$ name) name') u (Apply (Apply LookupSym0 name) (Apply SchSym0 attrs))
data LookupSym1 (l :: [AChar]) (l :: TyFun Schema U)
data LookupSym0 (k :: TyFun [AChar] (TyFun Schema U -> *))
type instance Apply (LookupSym1 a) a = Lookup a a
type instance Apply LookupSym0 a = LookupSym1 a
data instance Sing (z :: U)
= z ~ BOOL => SBOOL |
z ~ STRING => SSTRING |
z ~ NAT => SNAT |
forall (n :: U) (n :: Nat). z ~ VEC n n => SVEC (Sing n) (Sing n)
type SU (z :: U) = Sing z
instance SingKind (KProxy :: KProxy U) where
type instance DemoteRep (KProxy :: KProxy 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 b)
= case
(toSing b :: SomeSing (KProxy :: KProxy U),
toSing b :: SomeSing (KProxy :: KProxy Nat))
of {
(SomeSing c, SomeSing c) -> SomeSing (SVEC c c) }
instance SEq (KProxy :: KProxy U) where
%:== SBOOL SBOOL = STrue
%:== SBOOL SSTRING = SFalse
%:== SBOOL SNAT = SFalse
%:== SBOOL (SVEC _ _) = SFalse
%:== SSTRING SBOOL = SFalse
%:== SSTRING SSTRING = STrue
%:== SSTRING SNAT = SFalse
%:== SSTRING (SVEC _ _) = SFalse
%:== SNAT SBOOL = SFalse
%:== SNAT SSTRING = SFalse
%:== SNAT SNAT = STrue
%:== SNAT (SVEC _ _) = SFalse
%:== (SVEC _ _) SBOOL = SFalse
%:== (SVEC _ _) SSTRING = SFalse
%:== (SVEC _ _) SNAT = SFalse
%:== (SVEC a a) (SVEC b b) = (%:&&) ((%:==) a b) ((%:==) a b)
instance SDecide (KProxy :: KProxy U) where
%~ SBOOL SBOOL = Proved Refl
%~ SBOOL SSTRING
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SBOOL SNAT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SBOOL (SVEC _ _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SSTRING SBOOL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SSTRING SSTRING = Proved Refl
%~ SSTRING SNAT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SSTRING (SVEC _ _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SNAT SBOOL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SNAT SSTRING
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SNAT SNAT = Proved Refl
%~ SNAT (SVEC _ _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SVEC _ _) SBOOL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SVEC _ _) SSTRING
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SVEC _ _) SNAT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SVEC a a) (SVEC b b)
= case ((%~) a b, (%~) a b) of {
(Proved Refl, Proved Refl) -> Proved Refl
(Disproved contra, _) -> Disproved (\ Refl -> contra Refl)
(_, Disproved contra) -> Disproved (\ Refl -> contra Refl) }
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
data instance Sing (z :: AChar)
= z ~ CA => SCA |
z ~ CB => SCB |
z ~ CC => SCC |
z ~ CD => SCD |
z ~ CE => SCE |
z ~ CF => SCF |
z ~ CG => SCG |
z ~ CH => SCH |
z ~ CI => SCI |
z ~ CJ => SCJ |
z ~ CK => SCK |
z ~ CL => SCL |
z ~ CM => SCM |
z ~ CN => SCN |
z ~ CO => SCO |
z ~ CP => SCP |
z ~ CQ => SCQ |
z ~ CR => SCR |
z ~ CS => SCS |
z ~ CT => SCT |
z ~ CU => SCU |
z ~ CV => SCV |
z ~ CW => SCW |
z ~ CX => SCX |
z ~ CY => SCY |
z ~ CZ => SCZ
type SAChar (z :: AChar) = Sing z
instance SingKind (KProxy :: KProxy AChar) where
type instance DemoteRep (KProxy :: KProxy 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
instance SEq (KProxy :: KProxy AChar) where
%:== SCA SCA = STrue
%:== SCA SCB = SFalse
%:== SCA SCC = SFalse
%:== SCA SCD = SFalse
%:== SCA SCE = SFalse
%:== SCA SCF = SFalse
%:== SCA SCG = SFalse
%:== SCA SCH = SFalse
%:== SCA SCI = SFalse
%:== SCA SCJ = SFalse
%:== SCA SCK = SFalse
%:== SCA SCL = SFalse
%:== SCA SCM = SFalse
%:== SCA SCN = SFalse
%:== SCA SCO = SFalse
%:== SCA SCP = SFalse
%:== SCA SCQ = SFalse
%:== SCA SCR = SFalse
%:== SCA SCS = SFalse
%:== SCA SCT = SFalse
%:== SCA SCU = SFalse
%:== SCA SCV = SFalse
%:== SCA SCW = SFalse
%:== SCA SCX = SFalse
%:== SCA SCY = SFalse
%:== SCA SCZ = SFalse
%:== SCB SCA = SFalse
%:== SCB SCB = STrue
%:== SCB SCC = SFalse
%:== SCB SCD = SFalse
%:== SCB SCE = SFalse
%:== SCB SCF = SFalse
%:== SCB SCG = SFalse
%:== SCB SCH = SFalse
%:== SCB SCI = SFalse
%:== SCB SCJ = SFalse
%:== SCB SCK = SFalse
%:== SCB SCL = SFalse
%:== SCB SCM = SFalse
%:== SCB SCN = SFalse
%:== SCB SCO = SFalse
%:== SCB SCP = SFalse
%:== SCB SCQ = SFalse
%:== SCB SCR = SFalse
%:== SCB SCS = SFalse
%:== SCB SCT = SFalse
%:== SCB SCU = SFalse
%:== SCB SCV = SFalse
%:== SCB SCW = SFalse
%:== SCB SCX = SFalse
%:== SCB SCY = SFalse
%:== SCB SCZ = SFalse
%:== SCC SCA = SFalse
%:== SCC SCB = SFalse
%:== SCC SCC = STrue
%:== SCC SCD = SFalse
%:== SCC SCE = SFalse
%:== SCC SCF = SFalse
%:== SCC SCG = SFalse
%:== SCC SCH = SFalse
%:== SCC SCI = SFalse
%:== SCC SCJ = SFalse
%:== SCC SCK = SFalse
%:== SCC SCL = SFalse
%:== SCC SCM = SFalse
%:== SCC SCN = SFalse
%:== SCC SCO = SFalse
%:== SCC SCP = SFalse
%:== SCC SCQ = SFalse
%:== SCC SCR = SFalse
%:== SCC SCS = SFalse
%:== SCC SCT = SFalse
%:== SCC SCU = SFalse
%:== SCC SCV = SFalse
%:== SCC SCW = SFalse
%:== SCC SCX = SFalse
%:== SCC SCY = SFalse
%:== SCC SCZ = SFalse
%:== SCD SCA = SFalse
%:== SCD SCB = SFalse
%:== SCD SCC = SFalse
%:== SCD SCD = STrue
%:== SCD SCE = SFalse
%:== SCD SCF = SFalse
%:== SCD SCG = SFalse
%:== SCD SCH = SFalse
%:== SCD SCI = SFalse
%:== SCD SCJ = SFalse
%:== SCD SCK = SFalse
%:== SCD SCL = SFalse
%:== SCD SCM = SFalse
%:== SCD SCN = SFalse
%:== SCD SCO = SFalse
%:== SCD SCP = SFalse
%:== SCD SCQ = SFalse
%:== SCD SCR = SFalse
%:== SCD SCS = SFalse
%:== SCD SCT = SFalse
%:== SCD SCU = SFalse
%:== SCD SCV = SFalse
%:== SCD SCW = SFalse
%:== SCD SCX = SFalse
%:== SCD SCY = SFalse
%:== SCD SCZ = SFalse
%:== SCE SCA = SFalse
%:== SCE SCB = SFalse
%:== SCE SCC = SFalse
%:== SCE SCD = SFalse
%:== SCE SCE = STrue
%:== SCE SCF = SFalse
%:== SCE SCG = SFalse
%:== SCE SCH = SFalse
%:== SCE SCI = SFalse
%:== SCE SCJ = SFalse
%:== SCE SCK = SFalse
%:== SCE SCL = SFalse
%:== SCE SCM = SFalse
%:== SCE SCN = SFalse
%:== SCE SCO = SFalse
%:== SCE SCP = SFalse
%:== SCE SCQ = SFalse
%:== SCE SCR = SFalse
%:== SCE SCS = SFalse
%:== SCE SCT = SFalse
%:== SCE SCU = SFalse
%:== SCE SCV = SFalse
%:== SCE SCW = SFalse
%:== SCE SCX = SFalse
%:== SCE SCY = SFalse
%:== SCE SCZ = SFalse
%:== SCF SCA = SFalse
%:== SCF SCB = SFalse
%:== SCF SCC = SFalse
%:== SCF SCD = SFalse
%:== SCF SCE = SFalse
%:== SCF SCF = STrue
%:== SCF SCG = SFalse
%:== SCF SCH = SFalse
%:== SCF SCI = SFalse
%:== SCF SCJ = SFalse
%:== SCF SCK = SFalse
%:== SCF SCL = SFalse
%:== SCF SCM = SFalse
%:== SCF SCN = SFalse
%:== SCF SCO = SFalse
%:== SCF SCP = SFalse
%:== SCF SCQ = SFalse
%:== SCF SCR = SFalse
%:== SCF SCS = SFalse
%:== SCF SCT = SFalse
%:== SCF SCU = SFalse
%:== SCF SCV = SFalse
%:== SCF SCW = SFalse
%:== SCF SCX = SFalse
%:== SCF SCY = SFalse
%:== SCF SCZ = SFalse
%:== SCG SCA = SFalse
%:== SCG SCB = SFalse
%:== SCG SCC = SFalse
%:== SCG SCD = SFalse
%:== SCG SCE = SFalse
%:== SCG SCF = SFalse
%:== SCG SCG = STrue
%:== SCG SCH = SFalse
%:== SCG SCI = SFalse
%:== SCG SCJ = SFalse
%:== SCG SCK = SFalse
%:== SCG SCL = SFalse
%:== SCG SCM = SFalse
%:== SCG SCN = SFalse
%:== SCG SCO = SFalse
%:== SCG SCP = SFalse
%:== SCG SCQ = SFalse
%:== SCG SCR = SFalse
%:== SCG SCS = SFalse
%:== SCG SCT = SFalse
%:== SCG SCU = SFalse
%:== SCG SCV = SFalse
%:== SCG SCW = SFalse
%:== SCG SCX = SFalse
%:== SCG SCY = SFalse
%:== SCG SCZ = SFalse
%:== SCH SCA = SFalse
%:== SCH SCB = SFalse
%:== SCH SCC = SFalse
%:== SCH SCD = SFalse
%:== SCH SCE = SFalse
%:== SCH SCF = SFalse
%:== SCH SCG = SFalse
%:== SCH SCH = STrue
%:== SCH SCI = SFalse
%:== SCH SCJ = SFalse
%:== SCH SCK = SFalse
%:== SCH SCL = SFalse
%:== SCH SCM = SFalse
%:== SCH SCN = SFalse
%:== SCH SCO = SFalse
%:== SCH SCP = SFalse
%:== SCH SCQ = SFalse
%:== SCH SCR = SFalse
%:== SCH SCS = SFalse
%:== SCH SCT = SFalse
%:== SCH SCU = SFalse
%:== SCH SCV = SFalse
%:== SCH SCW = SFalse
%:== SCH SCX = SFalse
%:== SCH SCY = SFalse
%:== SCH SCZ = SFalse
%:== SCI SCA = SFalse
%:== SCI SCB = SFalse
%:== SCI SCC = SFalse
%:== SCI SCD = SFalse
%:== SCI SCE = SFalse
%:== SCI SCF = SFalse
%:== SCI SCG = SFalse
%:== SCI SCH = SFalse
%:== SCI SCI = STrue
%:== SCI SCJ = SFalse
%:== SCI SCK = SFalse
%:== SCI SCL = SFalse
%:== SCI SCM = SFalse
%:== SCI SCN = SFalse
%:== SCI SCO = SFalse
%:== SCI SCP = SFalse
%:== SCI SCQ = SFalse
%:== SCI SCR = SFalse
%:== SCI SCS = SFalse
%:== SCI SCT = SFalse
%:== SCI SCU = SFalse
%:== SCI SCV = SFalse
%:== SCI SCW = SFalse
%:== SCI SCX = SFalse
%:== SCI SCY = SFalse
%:== SCI SCZ = SFalse
%:== SCJ SCA = SFalse
%:== SCJ SCB = SFalse
%:== SCJ SCC = SFalse
%:== SCJ SCD = SFalse
%:== SCJ SCE = SFalse
%:== SCJ SCF = SFalse
%:== SCJ SCG = SFalse
%:== SCJ SCH = SFalse
%:== SCJ SCI = SFalse
%:== SCJ SCJ = STrue
%:== SCJ SCK = SFalse
%:== SCJ SCL = SFalse
%:== SCJ SCM = SFalse
%:== SCJ SCN = SFalse
%:== SCJ SCO = SFalse
%:== SCJ SCP = SFalse
%:== SCJ SCQ = SFalse
%:== SCJ SCR = SFalse
%:== SCJ SCS = SFalse
%:== SCJ SCT = SFalse
%:== SCJ SCU = SFalse
%:== SCJ SCV = SFalse
%:== SCJ SCW = SFalse
%:== SCJ SCX = SFalse
%:== SCJ SCY = SFalse
%:== SCJ SCZ = SFalse
%:== SCK SCA = SFalse
%:== SCK SCB = SFalse
%:== SCK SCC = SFalse
%:== SCK SCD = SFalse
%:== SCK SCE = SFalse
%:== SCK SCF = SFalse
%:== SCK SCG = SFalse
%:== SCK SCH = SFalse
%:== SCK SCI = SFalse
%:== SCK SCJ = SFalse
%:== SCK SCK = STrue
%:== SCK SCL = SFalse
%:== SCK SCM = SFalse
%:== SCK SCN = SFalse
%:== SCK SCO = SFalse
%:== SCK SCP = SFalse
%:== SCK SCQ = SFalse
%:== SCK SCR = SFalse
%:== SCK SCS = SFalse
%:== SCK SCT = SFalse
%:== SCK SCU = SFalse
%:== SCK SCV = SFalse
%:== SCK SCW = SFalse
%:== SCK SCX = SFalse
%:== SCK SCY = SFalse
%:== SCK SCZ = SFalse
%:== SCL SCA = SFalse
%:== SCL SCB = SFalse
%:== SCL SCC = SFalse
%:== SCL SCD = SFalse
%:== SCL SCE = SFalse
%:== SCL SCF = SFalse
%:== SCL SCG = SFalse
%:== SCL SCH = SFalse
%:== SCL SCI = SFalse
%:== SCL SCJ = SFalse
%:== SCL SCK = SFalse
%:== SCL SCL = STrue
%:== SCL SCM = SFalse
%:== SCL SCN = SFalse
%:== SCL SCO = SFalse
%:== SCL SCP = SFalse
%:== SCL SCQ = SFalse
%:== SCL SCR = SFalse
%:== SCL SCS = SFalse
%:== SCL SCT = SFalse
%:== SCL SCU = SFalse
%:== SCL SCV = SFalse
%:== SCL SCW = SFalse
%:== SCL SCX = SFalse
%:== SCL SCY = SFalse
%:== SCL SCZ = SFalse
%:== SCM SCA = SFalse
%:== SCM SCB = SFalse
%:== SCM SCC = SFalse
%:== SCM SCD = SFalse
%:== SCM SCE = SFalse
%:== SCM SCF = SFalse
%:== SCM SCG = SFalse
%:== SCM SCH = SFalse
%:== SCM SCI = SFalse
%:== SCM SCJ = SFalse
%:== SCM SCK = SFalse
%:== SCM SCL = SFalse
%:== SCM SCM = STrue
%:== SCM SCN = SFalse
%:== SCM SCO = SFalse
%:== SCM SCP = SFalse
%:== SCM SCQ = SFalse
%:== SCM SCR = SFalse
%:== SCM SCS = SFalse
%:== SCM SCT = SFalse
%:== SCM SCU = SFalse
%:== SCM SCV = SFalse
%:== SCM SCW = SFalse
%:== SCM SCX = SFalse
%:== SCM SCY = SFalse
%:== SCM SCZ = SFalse
%:== SCN SCA = SFalse
%:== SCN SCB = SFalse
%:== SCN SCC = SFalse
%:== SCN SCD = SFalse
%:== SCN SCE = SFalse
%:== SCN SCF = SFalse
%:== SCN SCG = SFalse
%:== SCN SCH = SFalse
%:== SCN SCI = SFalse
%:== SCN SCJ = SFalse
%:== SCN SCK = SFalse
%:== SCN SCL = SFalse
%:== SCN SCM = SFalse
%:== SCN SCN = STrue
%:== SCN SCO = SFalse
%:== SCN SCP = SFalse
%:== SCN SCQ = SFalse
%:== SCN SCR = SFalse
%:== SCN SCS = SFalse
%:== SCN SCT = SFalse
%:== SCN SCU = SFalse
%:== SCN SCV = SFalse
%:== SCN SCW = SFalse
%:== SCN SCX = SFalse
%:== SCN SCY = SFalse
%:== SCN SCZ = SFalse
%:== SCO SCA = SFalse
%:== SCO SCB = SFalse
%:== SCO SCC = SFalse
%:== SCO SCD = SFalse
%:== SCO SCE = SFalse
%:== SCO SCF = SFalse
%:== SCO SCG = SFalse
%:== SCO SCH = SFalse
%:== SCO SCI = SFalse
%:== SCO SCJ = SFalse
%:== SCO SCK = SFalse
%:== SCO SCL = SFalse
%:== SCO SCM = SFalse
%:== SCO SCN = SFalse
%:== SCO SCO = STrue
%:== SCO SCP = SFalse
%:== SCO SCQ = SFalse
%:== SCO SCR = SFalse
%:== SCO SCS = SFalse
%:== SCO SCT = SFalse
%:== SCO SCU = SFalse
%:== SCO SCV = SFalse
%:== SCO SCW = SFalse
%:== SCO SCX = SFalse
%:== SCO SCY = SFalse
%:== SCO SCZ = SFalse
%:== SCP SCA = SFalse
%:== SCP SCB = SFalse
%:== SCP SCC = SFalse
%:== SCP SCD = SFalse
%:== SCP SCE = SFalse
%:== SCP SCF = SFalse
%:== SCP SCG = SFalse
%:== SCP SCH = SFalse
%:== SCP SCI = SFalse
%:== SCP SCJ = SFalse
%:== SCP SCK = SFalse
%:== SCP SCL = SFalse
%:== SCP SCM = SFalse
%:== SCP SCN = SFalse
%:== SCP SCO = SFalse
%:== SCP SCP = STrue
%:== SCP SCQ = SFalse
%:== SCP SCR = SFalse
%:== SCP SCS = SFalse
%:== SCP SCT = SFalse
%:== SCP SCU = SFalse
%:== SCP SCV = SFalse
%:== SCP SCW = SFalse
%:== SCP SCX = SFalse
%:== SCP SCY = SFalse
%:== SCP SCZ = SFalse
%:== SCQ SCA = SFalse
%:== SCQ SCB = SFalse
%:== SCQ SCC = SFalse
%:== SCQ SCD = SFalse
%:== SCQ SCE = SFalse
%:== SCQ SCF = SFalse
%:== SCQ SCG = SFalse
%:== SCQ SCH = SFalse
%:== SCQ SCI = SFalse
%:== SCQ SCJ = SFalse
%:== SCQ SCK = SFalse
%:== SCQ SCL = SFalse
%:== SCQ SCM = SFalse
%:== SCQ SCN = SFalse
%:== SCQ SCO = SFalse
%:== SCQ SCP = SFalse
%:== SCQ SCQ = STrue
%:== SCQ SCR = SFalse
%:== SCQ SCS = SFalse
%:== SCQ SCT = SFalse
%:== SCQ SCU = SFalse
%:== SCQ SCV = SFalse
%:== SCQ SCW = SFalse
%:== SCQ SCX = SFalse
%:== SCQ SCY = SFalse
%:== SCQ SCZ = SFalse
%:== SCR SCA = SFalse
%:== SCR SCB = SFalse
%:== SCR SCC = SFalse
%:== SCR SCD = SFalse
%:== SCR SCE = SFalse
%:== SCR SCF = SFalse
%:== SCR SCG = SFalse
%:== SCR SCH = SFalse
%:== SCR SCI = SFalse
%:== SCR SCJ = SFalse
%:== SCR SCK = SFalse
%:== SCR SCL = SFalse
%:== SCR SCM = SFalse
%:== SCR SCN = SFalse
%:== SCR SCO = SFalse
%:== SCR SCP = SFalse
%:== SCR SCQ = SFalse
%:== SCR SCR = STrue
%:== SCR SCS = SFalse
%:== SCR SCT = SFalse
%:== SCR SCU = SFalse
%:== SCR SCV = SFalse
%:== SCR SCW = SFalse
%:== SCR SCX = SFalse
%:== SCR SCY = SFalse
%:== SCR SCZ = SFalse
%:== SCS SCA = SFalse
%:== SCS SCB = SFalse
%:== SCS SCC = SFalse
%:== SCS SCD = SFalse
%:== SCS SCE = SFalse
%:== SCS SCF = SFalse
%:== SCS SCG = SFalse
%:== SCS SCH = SFalse
%:== SCS SCI = SFalse
%:== SCS SCJ = SFalse
%:== SCS SCK = SFalse
%:== SCS SCL = SFalse
%:== SCS SCM = SFalse
%:== SCS SCN = SFalse
%:== SCS SCO = SFalse
%:== SCS SCP = SFalse
%:== SCS SCQ = SFalse
%:== SCS SCR = SFalse
%:== SCS SCS = STrue
%:== SCS SCT = SFalse
%:== SCS SCU = SFalse
%:== SCS SCV = SFalse
%:== SCS SCW = SFalse
%:== SCS SCX = SFalse
%:== SCS SCY = SFalse
%:== SCS SCZ = SFalse
%:== SCT SCA = SFalse
%:== SCT SCB = SFalse
%:== SCT SCC = SFalse
%:== SCT SCD = SFalse
%:== SCT SCE = SFalse
%:== SCT SCF = SFalse
%:== SCT SCG = SFalse
%:== SCT SCH = SFalse
%:== SCT SCI = SFalse
%:== SCT SCJ = SFalse
%:== SCT SCK = SFalse
%:== SCT SCL = SFalse
%:== SCT SCM = SFalse
%:== SCT SCN = SFalse
%:== SCT SCO = SFalse
%:== SCT SCP = SFalse
%:== SCT SCQ = SFalse
%:== SCT SCR = SFalse
%:== SCT SCS = SFalse
%:== SCT SCT = STrue
%:== SCT SCU = SFalse
%:== SCT SCV = SFalse
%:== SCT SCW = SFalse
%:== SCT SCX = SFalse
%:== SCT SCY = SFalse
%:== SCT SCZ = SFalse
%:== SCU SCA = SFalse
%:== SCU SCB = SFalse
%:== SCU SCC = SFalse
%:== SCU SCD = SFalse
%:== SCU SCE = SFalse
%:== SCU SCF = SFalse
%:== SCU SCG = SFalse
%:== SCU SCH = SFalse
%:== SCU SCI = SFalse
%:== SCU SCJ = SFalse
%:== SCU SCK = SFalse
%:== SCU SCL = SFalse
%:== SCU SCM = SFalse
%:== SCU SCN = SFalse
%:== SCU SCO = SFalse
%:== SCU SCP = SFalse
%:== SCU SCQ = SFalse
%:== SCU SCR = SFalse
%:== SCU SCS = SFalse
%:== SCU SCT = SFalse
%:== SCU SCU = STrue
%:== SCU SCV = SFalse
%:== SCU SCW = SFalse
%:== SCU SCX = SFalse
%:== SCU SCY = SFalse
%:== SCU SCZ = SFalse
%:== SCV SCA = SFalse
%:== SCV SCB = SFalse
%:== SCV SCC = SFalse
%:== SCV SCD = SFalse
%:== SCV SCE = SFalse
%:== SCV SCF = SFalse
%:== SCV SCG = SFalse
%:== SCV SCH = SFalse
%:== SCV SCI = SFalse
%:== SCV SCJ = SFalse
%:== SCV SCK = SFalse
%:== SCV SCL = SFalse
%:== SCV SCM = SFalse
%:== SCV SCN = SFalse
%:== SCV SCO = SFalse
%:== SCV SCP = SFalse
%:== SCV SCQ = SFalse
%:== SCV SCR = SFalse
%:== SCV SCS = SFalse
%:== SCV SCT = SFalse
%:== SCV SCU = SFalse
%:== SCV SCV = STrue
%:== SCV SCW = SFalse
%:== SCV SCX = SFalse
%:== SCV SCY = SFalse
%:== SCV SCZ = SFalse
%:== SCW SCA = SFalse
%:== SCW SCB = SFalse
%:== SCW SCC = SFalse
%:== SCW SCD = SFalse
%:== SCW SCE = SFalse
%:== SCW SCF = SFalse
%:== SCW SCG = SFalse
%:== SCW SCH = SFalse
%:== SCW SCI = SFalse
%:== SCW SCJ = SFalse
%:== SCW SCK = SFalse
%:== SCW SCL = SFalse
%:== SCW SCM = SFalse
%:== SCW SCN = SFalse
%:== SCW SCO = SFalse
%:== SCW SCP = SFalse
%:== SCW SCQ = SFalse
%:== SCW SCR = SFalse
%:== SCW SCS = SFalse
%:== SCW SCT = SFalse
%:== SCW SCU = SFalse
%:== SCW SCV = SFalse
%:== SCW SCW = STrue
%:== SCW SCX = SFalse
%:== SCW SCY = SFalse
%:== SCW SCZ = SFalse
%:== SCX SCA = SFalse
%:== SCX SCB = SFalse
%:== SCX SCC = SFalse
%:== SCX SCD = SFalse
%:== SCX SCE = SFalse
%:== SCX SCF = SFalse
%:== SCX SCG = SFalse
%:== SCX SCH = SFalse
%:== SCX SCI = SFalse
%:== SCX SCJ = SFalse
%:== SCX SCK = SFalse
%:== SCX SCL = SFalse
%:== SCX SCM = SFalse
%:== SCX SCN = SFalse
%:== SCX SCO = SFalse
%:== SCX SCP = SFalse
%:== SCX SCQ = SFalse
%:== SCX SCR = SFalse
%:== SCX SCS = SFalse
%:== SCX SCT = SFalse
%:== SCX SCU = SFalse
%:== SCX SCV = SFalse
%:== SCX SCW = SFalse
%:== SCX SCX = STrue
%:== SCX SCY = SFalse
%:== SCX SCZ = SFalse
%:== SCY SCA = SFalse
%:== SCY SCB = SFalse
%:== SCY SCC = SFalse
%:== SCY SCD = SFalse
%:== SCY SCE = SFalse
%:== SCY SCF = SFalse
%:== SCY SCG = SFalse
%:== SCY SCH = SFalse
%:== SCY SCI = SFalse
%:== SCY SCJ = SFalse
%:== SCY SCK = SFalse
%:== SCY SCL = SFalse
%:== SCY SCM = SFalse
%:== SCY SCN = SFalse
%:== SCY SCO = SFalse
%:== SCY SCP = SFalse
%:== SCY SCQ = SFalse
%:== SCY SCR = SFalse
%:== SCY SCS = SFalse
%:== SCY SCT = SFalse
%:== SCY SCU = SFalse
%:== SCY SCV = SFalse
%:== SCY SCW = SFalse
%:== SCY SCX = SFalse
%:== SCY SCY = STrue
%:== SCY SCZ = SFalse
%:== SCZ SCA = SFalse
%:== SCZ SCB = SFalse
%:== SCZ SCC = SFalse
%:== SCZ SCD = SFalse
%:== SCZ SCE = SFalse
%:== SCZ SCF = SFalse
%:== SCZ SCG = SFalse
%:== SCZ SCH = SFalse
%:== SCZ SCI = SFalse
%:== SCZ SCJ = SFalse
%:== SCZ SCK = SFalse
%:== SCZ SCL = SFalse
%:== SCZ SCM = SFalse
%:== SCZ SCN = SFalse
%:== SCZ SCO = SFalse
%:== SCZ SCP = SFalse
%:== SCZ SCQ = SFalse
%:== SCZ SCR = SFalse
%:== SCZ SCS = SFalse
%:== SCZ SCT = SFalse
%:== SCZ SCU = SFalse
%:== SCZ SCV = SFalse
%:== SCZ SCW = SFalse
%:== SCZ SCX = SFalse
%:== SCZ SCY = SFalse
%:== SCZ SCZ = STrue
instance SDecide (KProxy :: KProxy AChar) where
%~ SCA SCA = Proved Refl
%~ SCA SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCA SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCB = Proved Refl
%~ SCB SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCB SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCC = Proved Refl
%~ SCC SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCC SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCD = Proved Refl
%~ SCD SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCD SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCE = Proved Refl
%~ SCE SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCE SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCF = Proved Refl
%~ SCF SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCF SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCG = Proved Refl
%~ SCG SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCG SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCH = Proved Refl
%~ SCH SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCH SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCI = Proved Refl
%~ SCI SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCI SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCJ = Proved Refl
%~ SCJ SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCJ SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCK = Proved Refl
%~ SCK SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCK SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCL = Proved Refl
%~ SCL SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCL SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCM = Proved Refl
%~ SCM SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCM SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCN = Proved Refl
%~ SCN SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCN SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCO = Proved Refl
%~ SCO SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCO SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCP = Proved Refl
%~ SCP SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCP SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCQ = Proved Refl
%~ SCQ SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCQ SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCR = Proved Refl
%~ SCR SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCR SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCS = Proved Refl
%~ SCS SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCS SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCT = Proved Refl
%~ SCT SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCT SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCU = Proved Refl
%~ SCU SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCU SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCV = Proved Refl
%~ SCV SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCV SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCW = Proved Refl
%~ SCW SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCW SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCX = Proved Refl
%~ SCX SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCX SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCY SCY = Proved Refl
%~ SCY SCZ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCA
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCB
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCC
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCD
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCE
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCF
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCG
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCH
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCI
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCJ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCK
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCL
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCM
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCN
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCO
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCP
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCQ
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCR
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCS
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCT
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCU
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCV
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCW
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCX
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCY
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SCZ SCZ = Proved Refl
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
data instance Sing (z :: Attribute)
= forall (n :: [AChar]) (n :: U). z ~ Attr n n =>
SAttr (Sing n) (Sing n)
type SAttribute (z :: Attribute) = Sing z
instance SingKind (KProxy :: KProxy Attribute) where
type instance DemoteRep (KProxy :: KProxy Attribute) = Attribute
fromSing (SAttr b b) = Attr (fromSing b) (fromSing b)
toSing (Attr b b)
= case
(toSing b :: SomeSing (KProxy :: KProxy [AChar]),
toSing b :: SomeSing (KProxy :: KProxy U))
of {
(SomeSing c, SomeSing c) -> SomeSing (SAttr c c) }
instance (SingI n, SingI n) =>
SingI (Attr (n :: [AChar]) (n :: U)) where
sing = SAttr sing sing
data instance Sing (z :: Schema)
= forall (n :: [Attribute]). z ~ Sch n => SSch (Sing n)
type SSchema (z :: Schema) = Sing z
instance SingKind (KProxy :: KProxy Schema) where
type instance DemoteRep (KProxy :: KProxy Schema) = Schema
fromSing (SSch b) = Sch (fromSing b)
toSing (Sch b)
= case toSing b :: SomeSing (KProxy :: KProxy [Attribute]) of {
SomeSing c -> SomeSing (SSch c) }
instance SingI n => SingI (Sch (n :: [Attribute])) where
sing = SSch sing
sAppend ::
forall (t :: Schema) (t :: Schema).
Sing t -> Sing t -> Sing (Append t t)
sAppend (SSch s1) (SSch s2) = SSch ((%:++) s1 s2)
sAttrNotIn ::
forall (t :: Attribute) (t :: Schema).
Sing t -> Sing t -> Sing (AttrNotIn t t)
sAttrNotIn _ (SSch SNil) = STrue
sAttrNotIn (SAttr name u) (SSch (SCons (SAttr name' _) t))
= (%:&&) ((%:/=) name name') (sAttrNotIn (SAttr name u) (SSch t))
sDisjoint ::
forall (t :: Schema) (t :: Schema).
Sing t -> Sing t -> Sing (Disjoint t t)
sDisjoint (SSch SNil) _ = STrue
sDisjoint (SSch (SCons h t)) s
= (%:&&) (sAttrNotIn h s) (sDisjoint (SSch t) s)
sOccurs ::
forall (t :: [AChar]) (t :: Schema).
Sing t -> Sing t -> Sing (Occurs t t)
sOccurs _ (SSch SNil) = SFalse
sOccurs name (SSch (SCons (SAttr name' _) attrs))
= (%:||) ((%:==) name name') (sOccurs name (SSch attrs))
sLookup ::
forall (t :: [AChar]) (t :: Schema).
Sing t -> Sing t -> Sing (Lookup t t)
sLookup _ (SSch SNil) = undefined
sLookup name (SSch (SCons (SAttr name' u) attrs))
= sIf ((%:==) name name') u (sLookup name (SSch attrs))
GradingClient/Database.hs:0:0: Splicing declarations
return [] ======> GradingClient/Database.hs:0:0:
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 }