1 files changed, 74 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lem_stringScript.sml b/snapshots/hol4/lem/hol-lib/lem_stringScript.sml
new file mode 100644
index 00000000..9dd53778
--- /dev/null
+++ b/snapshots/hol4/lem/hol-lib/lem_stringScript.sml
@@ -0,0 +1,74 @@
+(*Generated by Lem from string.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_listTheory lemTheory stringTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_string"
+
+
+
+(*open import Bool Basic_classes List*)
+(*open import {ocaml} `Xstring`*)
+(*open import {hol} `lemTheory` `stringTheory`*)
+(*open import {coq} `Coq.Strings.Ascii` `Coq.Strings.String`*)
+
+(* ------------------------------------------- *)
+(* translations between strings and char lists *)
+(* ------------------------------------------- *)
+
+(*val toCharList : string -> list char*)
+
+(*val toString : list char -> string*)
+
+
+(* ----------------------- *)
+(* generating strings      *)
+(* ----------------------- *)
+
+(*val makeString : nat -> char -> string*)
+(*let makeString len c=  toString (replicate len c)*)
+
+(* ----------------------- *)
+(* length                  *)
+(* ----------------------- *)
+
+(*val stringLength : string -> nat*)
+
+(* ----------------------- *)
+(* string concatenation    *)
+(* ----------------------- *)
+
+(*val ^ [stringAppend] : string -> string -> string*)
+
+
+(* ----------------------------*)
+(* setting up pattern matching *)
+(* --------------------------- *)
+
+(*val string_case : forall 'a. string -> 'a -> (char -> string -> 'a) -> 'a*)
+
+(*let string_case s c_empty c_cons= 
+  match (toCharList s) with
+    | [] -> c_empty
+    | c :: cs -> c_cons c (toString cs)
+  end*)
+
+(*val empty_string : string*)
+
+(*val cons_string : char -> string -> string*)
+
+(*val concat : string -> list string -> string*)
+ val concat_defn = Defn.Hol_multi_defns `
+ ((concat:string ->(string)list -> string) sep ([])=  "")
+/\ ((concat:string ->(string)list -> string) sep (s :: ss')=      
+ ((case ss' of
+        [] => s
+      | _ =>  STRCAT s  (STRCAT sep (concat sep ss'))
+      )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) concat_defn;
+val _ = export_theory()
+