From 1c8f2fb8ce8692dc5d0c1b0af045a34337c5350e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 12 Jan 2016 14:25:35 +0100
Subject: [PATCH] Tail recursive reverse operation on strings.

---
 theories/strings.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/strings.v b/theories/strings.v
index e6c0294a..fd41ea2d 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -16,6 +16,14 @@ Proof. solve_decision. Defined.
 Instance: Injective (=) (=) (String.append s1).
 Proof. intros s1 ???. induction s1; simplify_equality'; f_equal'; auto. Qed.
 
+(* Reverse *)
+Fixpoint string_rev_app (s1 s2 : string) : string :=
+  match s1 with
+  | "" => s2
+  | String a s1 => string_rev_app s1 (String a s2)
+  end.
+Definition string_rev (s : string) : string := string_rev_app s "".
+
 (** * Encoding and decoding *)
 (** In order to reuse or existing implementation of radix-2 search trees over
 positive binary naturals [positive], we define an injection [string_to_pos]
-- 
GitLab