1) PTS simplified

[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..ea1c1ccd145b9e21d50a6ecb82b2f957eb5f53e0 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 *)
 (* ************ *)
@@ -65,7 +51,7 @@ ndefinition strLen_str ≝ len_list ascii.
 ninductive aux_strId_type : Type ≝
  STR_ID: aux_str_type → nat → aux_strId_type.
 
-ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
+(*ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
 λP:aux_strId_type → Prop.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
  match a with [ STR_ID l n ⇒ f l n ].
 
@@ -75,7 +61,7 @@ ndefinition aux_strId_type_rec : ΠP:aux_strId_type → Set.(Πl,n.P (STR_ID l n
 
 ndefinition aux_strId_type_rect : ΠP:aux_strId_type → Type.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
 λP:aux_strId_type → Type.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
- match a with [ STR_ID l n ⇒ f l n ].
+ match a with [ STR_ID l n ⇒ f l n ].*)
 
 (* getter *)
 ndefinition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].