Merge PR #6744: Add String.concat

1 files changed, 12 insertions, 0 deletions

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] *)