Concrete spaces do form a category, after all :-)

[helm.git] / helm / software / matita / contribs / assembly / string / string.ma

diff --git a/helm/software/matita/contribs/assembly/string/string.ma b/helm/software/matita/contribs/assembly/string/string.ma
index 0a81fb6e6c147476579004613f948507a3f7f36c..f60b8a804c46f3a7bb5d42de6de1ffd1db4355ac 100755 (executable)
--- a/helm/software/matita/contribs/assembly/string/string.ma
+++ b/helm/software/matita/contribs/assembly/string/string.ma
@@ -48,9 +48,27 @@ let rec strCmp_str (str,str':aux_str_type) ≝
     [ true ⇒ strCmp_str t t' | false ⇒ false ]
   ]].
 
+axiom eqbstrcmpstr_to_eq : ∀s,s'.strCmp_str s s' = true → s = s'.
+
 (* strcat *)
 definition strCat_str ≝
 λstr,str':aux_str_type.str@str'.
 
 (* strlen *)
 definition strLen_str ≝ λstr:aux_str_type.len_list ? str.
+
+(* ************ *)
+(* STRINGA + ID *)
+(* ************ *)
+
+(* tipo pubblico *)
+inductive aux_strId_type : Type ≝
+ STR_ID: aux_str_type → nat → aux_strId_type.
+
+(* getter *)
+definition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
+definition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ].
+
+(* confronto *)
+definition strCmp_strId ≝
+λsid,sid':aux_strId_type.(strCmp_str (get_name_strId sid) (get_name_strId sid'))⊗(eqb (get_id_strId sid) (get_id_strId sid')).