1 files changed, 85 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lem_showScript.sml b/snapshots/hol4/lem/hol-lib/lem_showScript.sml
new file mode 100644
index 00000000..1852c219
--- /dev/null
+++ b/snapshots/hol4/lem/hol-lib/lem_showScript.sml
@@ -0,0 +1,85 @@
+(*Generated by Lem from show.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_stringTheory lem_maybeTheory lem_numTheory lem_basic_classesTheory lemTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_show"
+
+
+
+(*open import String Maybe Num Basic_classes*)
+
+(*open import {hol} `lemTheory`*)
+
+val _ = Hol_datatype `
+(*  'a *) Show_class= <|
+  show_method: 'a -> string
+|>`;
+
+
+val _ = Define `
+((instance_Show_Show_string_dict:(string)Show_class)= (<|
+
+  show_method := (\ s.  STRCAT"\""  (STRCAT s "\""))|>))`;
+
+
+(*val stringFromMaybe : forall 'a. ('a -> string) -> Maybe.maybe 'a -> string*)
+val _ = Define `
+ ((stringFromMaybe:('a -> string) -> 'a option -> string) showX (SOME x)=   (STRCAT"Just ("  (STRCAT(showX x) ")")))
+/\ ((stringFromMaybe:('a -> string) -> 'a option -> string) showX NONE=  "Nothing")`;
+
+
+val _ = Define `
+((instance_Show_Show_Maybe_maybe_dict:'a Show_class ->('a option)Show_class)dict_Show_Show_a= (<|
+
+  show_method := (\ x_opt. stringFromMaybe  
+  dict_Show_Show_a.show_method x_opt)|>))`;
+
+
+(*val stringFromListAux : forall 'a. ('a -> string) -> list 'a -> string*)
+ val stringFromListAux_defn = Defn.Hol_multi_defns `
+ ((stringFromListAux:('a -> string) -> 'a list -> string) showX ([])=  "")
+/\ ((stringFromListAux:('a -> string) -> 'a list -> string) showX (x::xs')=      
+ ((case xs' of
+        [] => showX x
+      | _ =>  STRCAT(showX x)  (STRCAT"; " (stringFromListAux showX xs'))
+      )))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) stringFromListAux_defn;
+
+(*val stringFromList : forall 'a. ('a -> string) -> list 'a -> string*)
+val _ = Define `
+ ((stringFromList:('a -> string) -> 'a list -> string) showX xs=   
+ (STRCAT"["  (STRCAT(stringFromListAux showX xs) "]")))`;
+
+
+val _ = Define `
+((instance_Show_Show_list_dict:'a Show_class ->('a list)Show_class)dict_Show_Show_a= (<|
+
+  show_method := (\ xs. stringFromList  
+  dict_Show_Show_a.show_method xs)|>))`;
+
+
+(*val stringFromPair : forall 'a 'b. ('a -> string) -> ('b -> string) -> ('a * 'b) -> string*)
+val _ = Define `
+ ((stringFromPair:('a -> string) ->('b -> string) -> 'a#'b -> string) showX showY (x,y)=   
+ (STRCAT"("  (STRCAT(showX x)  (STRCAT", "  (STRCAT(showY y) ")")))))`;
+
+
+val _ = Define `
+((instance_Show_Show_tup2_dict:'a Show_class -> 'b Show_class ->('a#'b)Show_class)dict_Show_Show_a dict_Show_Show_b= (<|
+
+  show_method := (stringFromPair  
+  dict_Show_Show_a.show_method  dict_Show_Show_b.show_method)|>))`;
+
+
+val _ = Define `
+((instance_Show_Show_bool_dict:(bool)Show_class)= (<|
+
+  show_method := (\ b. if b then "true" else "false")|>))`;
+
+val _ = export_theory()
+