From 6e3f45cf27bea67dd87ed824396a662f904c93e8 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 12 Feb 2018 13:28:39 -0500
Subject: Add String.concat

---
 CHANGES                   |  2 ++
 theories/Strings/String.v | 12 ++++++++++++
 2 files changed, 14 insertions(+)

diff --git a/CHANGES b/CHANGES
index 2040c1b57..e2970dfc7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -107,6 +107,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
 
 Changes from 8.7.1 to 8.7.2
 ===========================
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index c39b47fb1..d5852345b 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -163,6 +163,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] *)
-- 
cgit v1.2.3