blob: f91a4cb0472690949b32e88c56199d0892e8da73 (
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
|
(*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()
|
