X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Futility%2Fstring.ma;h=736bbf72238f4427a0e737e43031c059bcd6eaca;hb=f4f44aa85f6d8ad07c44ce5890bd447f04b9c8a2;hp=ea1c1ccd145b9e21d50a6ecb82b2f957eb5f53e0;hpb=33b04453963755b619ac644f988e86a09cd54d63;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/utility/string.ma b/helm/software/matita/contribs/ng_assembly/utility/string.ma
index ea1c1ccd1..736bbf722 100644
--- a/helm/software/matita/contribs/ng_assembly/utility/string.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/string.ma
@@ -23,6 +23,7 @@
 include "utility/ascii.ma".
 include "freescale/theory.ma".
 include "freescale/nat.ma".
+include "utility/utility.ma".
 
 (* ************************ *)
 (* MANIPOLAZIONE DI STRINGA *)
@@ -32,41 +33,22 @@ include "freescale/nat.ma".
 ndefinition aux_str_type ≝ list ascii.
 
 (* strcmp *)
-nlet rec eq_str (str,str':aux_str_type) ≝
- match str with
-  [ nil ⇒ match str' with
-   [ nil => true
-   | cons _ _ => false ]
-  | cons h t ⇒ match str' with
-   [ nil ⇒ false
-   | cons h' t' ⇒ (eq_ascii h h')⊗(eq_str t t')
-   ]
-  ].
+ndefinition eq_str ≝
+ bfold_right_list2 ascii (λx,y.eq_ascii x y).
 
 (* ************ *)
 (* STRINGA + ID *)
 (* ************ *)
 
 (* tipo pubblico *)
-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 ≝
-λ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 ].
-
-ndefinition aux_strId_type_rec : ΠP:aux_strId_type → Set.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
-λP:aux_strId_type → Set.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
- match a with [ STR_ID l n ⇒ f 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 ].*)
-
-(* getter *)
-ndefinition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
-ndefinition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ].
+nrecord strId : Type ≝
+ {
+ str_elem: aux_str_type;
+ id_elem: nat
+ }.
 
 (* confronto *)
 ndefinition eq_strId ≝
-λsid,sid':aux_strId_type.(eq_str (get_name_strId sid) (get_name_strId sid'))⊗(eq_nat (get_id_strId sid) (get_id_strId sid')).
+λsid,sid':strId.
+ (eq_str (str_elem sid) (str_elem sid'))⊗
+ (eq_nat (id_elem sid) (id_elem sid')).