aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES2
-rw-r--r--theories/Strings/String.v12
2 files changed, 14 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index ab6aab0ee..eaceea6da 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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] *)