Rename Dim -> Dimension.

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

diff --git a/symantic-lib/Language/Symantic/Lib/Integer.hs b/symantic-lib/Language/Symantic/Lib/Integer.hs
index e53a4995e1a9875ebb5902e4372af7f7dc80f2ee..60a846a1fbbe79e46035f29346b9539c6f77307b 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Integer.hs
+++ b/symantic-lib/Language/Symantic/Lib/Integer.hs
@@ -28,8 +28,10 @@ instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (Dup r1 r2) where
 instance (Sym_Integer term, Sym_Lambda term) => Sym_Integer (BetaT term)
 
 -- Typing
+instance NameTyOf Integer where
+       nameTyOf _c = ["Integer"] `Mod` "Integer"
 instance ClassInstancesFor Integer where
-       proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
+       proveConstraintFor _ (TyConst _ _ q :$ z)
         | Just HRefl <- proj_ConstKiTy @_ @Integer z
         = case () of
                 _ | Just Refl <- proj_Const @Enum     q -> Just Dict
@@ -50,19 +52,19 @@ instance
  , Gram_AltApp g
  , Gram_Rule g
  , Gram_Comment g
- , Inj_Sym ss Integer
+ , SymInj ss Integer
  ) => Gram_Term_AtomsFor src ss g Integer where
        g_term_atomsFor =
         [ rule "teinteger" $
-               lexeme $ g_source $
+               lexeme $ source $
                (\i src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teInteger $ read i)
                 <$> some (choice $ char <$> ['0'..'9'])
         ]
 instance ModuleFor src ss Integer
 
 -- ** 'Term's
-tyInteger :: Source src => Inj_Len vs => Type src vs Integer
+tyInteger :: Source src => LenInj vs => Type src vs Integer
 tyInteger = tyConst @(K Integer) @Integer
 
-teInteger :: Source src => Inj_Sym ss Integer => Integer -> Term src ss ts '[] (() #> Integer)
+teInteger :: Source src => SymInj ss Integer => Integer -> Term src ss ts '[] (() #> Integer)
 teInteger i = Term noConstraint tyInteger $ teSym @Integer $ integer i