From 6e3f45cf27bea67dd87ed824396a662f904c93e8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 12 Feb 2018 13:28:39 -0500 Subject: Add String.concat --- theories/Strings/String.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'theories') 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