freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / utility / string.ma

diff --git a/helm/software/matita/contribs/ng_assembly/utility/string.ma b/helm/software/matita/contribs/ng_assembly/utility/string.ma
index 227f9f478d2cb285d09c501be7cc7e712ded1371..d2a55290124d6b60ac9ba2a317c6daf21f1aca62 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/utility/string.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/string.ma
@@ -21,7 +21,8 @@
 (* ********************************************************************** *)
 
 include "utility/ascii.ma".
-include "utility/utility.ma".
+include "freescale/theory.ma".
+include "freescale/nat.ma".
 
 (* ************************ *)
 (* MANIPOLAZIONE DI STRINGA *)
@@ -30,14 +31,6 @@ include "utility/utility.ma".
 (* tipo pubblico *)
 ndefinition aux_str_type ≝ list ascii.
 
-(* empty string *)
-ndefinition empty_str ≝ nil ascii.
-
-(* is empty ? *)
-ndefinition isNull_str ≝
-λstr:aux_str_type.match str with
- [ nil ⇒ true | cons _ _ ⇒ false ].
-
 (* strcmp *)
 nlet rec eq_str (str,str':aux_str_type) ≝
  match str with
@@ -50,13 +43,6 @@ nlet rec eq_str (str,str':aux_str_type) ≝
    ]
   ].
 
-(* strcat *)
-ndefinition strCat_str ≝
-λstr,str':aux_str_type.str@str'.
-
-(* strlen *)
-ndefinition strLen_str ≝ len_list ascii.
-
 (* ************ *)
 (* STRINGA + ID *)
 (* ************ *)