blob: eef2c93e8fcae2f0043469fbaddab03854aee598 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
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 '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()
|
