Add colorable and decorable.

[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Bool.hs

diff --git a/symantic-lib/Language/Symantic/Lib/Bool.hs b/symantic-lib/Language/Symantic/Lib/Bool.hs
index 34820fc404c7093938f1d80ecf13e64907f35a69..88c27a27074d8093c28ce93015e0dfd040241d93 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Bool.hs
+++ b/symantic-lib/Language/Symantic/Lib/Bool.hs
@@ -55,9 +55,11 @@ instance (Sym_Lambda term, Sym_Bool term) => Sym_Bool (BetaT term) where
        xor = trans2 xor
 
 -- Typing
+instance NameTyOf Bool where
+       nameTyOf _c = ["Bool"] `Mod` "Bool"
 instance ClassInstancesFor Bool where
-       proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
-        | Just HRefl <- proj_ConstKiTy @_ @Bool c
+       proveConstraintFor _ (TyConst _ _ q :@ b)
+        | Just HRefl <- proj_ConstKiTy @_ @Bool b
         = case () of
                 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
                   | Just Refl <- proj_Const @Enum    q -> Just Dict
@@ -70,7 +72,7 @@ instance TypeInstancesFor Bool
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Bool
-instance (Source src, Inj_Sym ss Bool) => ModuleFor src ss Bool where
+instance (Source src, SymInj ss Bool) => ModuleFor src ss Bool where
        moduleFor = ["Bool"] `moduleWhere`
         [ "False" := teBool False
         , "True"  := teBool True
@@ -81,11 +83,11 @@ instance (Source src, Inj_Sym ss Bool) => ModuleFor src ss Bool where
         ]
 
 -- ** 'Type's
-tyBool :: Source src => Inj_Len vs => Type src vs Bool
+tyBool :: Source src => LenInj vs => Type src vs Bool
 tyBool = tyConst @(K Bool) @Bool
 
 -- ** 'Term's
-teBool :: Source src => Inj_Sym ss Bool => Bool -> Term src ss ts '[] (() #> Bool)
+teBool :: Source src => SymInj ss Bool => Bool -> Term src ss ts '[] (() #> Bool)
 teBool b = Term noConstraint tyBool $ teSym @Bool $ bool b
 
 teBool_not :: TermDef Bool '[] (() #> (Bool -> Bool))