diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | theories/Strings/String.v | 12 |
2 files changed, 14 insertions, 0 deletions
@@ -112,6 +112,8 @@ Standard Library Coq.Numbers.DecimalString providing a type of decimal numbers, some facts about them, and conversions between decimal numbers and nat, positive, N, Z, and string. +- Added [Coq.Strings.String.concat] to concatenate a list of strings + inserting a separator between each item - Some deprecated aliases are now emitting warnings when used. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index a302b8329..2be6618ad 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -165,6 +165,18 @@ intros n0 H; apply Rec; simpl; auto. apply Le.le_S_n; auto. Qed. +(** *** Concatenating lists of strings *) + +(** [concat sep sl] concatenates the list of strings [sl], inserting + the separator string [sep] between each. *) + +Fixpoint concat (sep : string) (ls : list string) := + match ls with + | nil => EmptyString + | cons x nil => x + | cons x xs => x ++ sep ++ concat sep xs + end. + (** *** Test functions *) (** Test if [s1] is a prefix of [s2] *) |