(*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 '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()