chapter ‹Generated by Lem from ‹string.lem›.› theory "Lem_string" imports Main "Lem_bool" "Lem_basic_classes" "Lem_list" begin ― ‹‹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›› function (sequential,domintros) concat :: " string ⇒(string)list ⇒ string " where " concat sep ([]) = ( (''''))" |" concat sep (s # ss') = ( (case ss' of [] => s | _ => s @ (sep @ concat sep ss') ))" by pat_completeness auto end