From 30cc675d57492799644506f3632625f371a3e89a Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 19 Mar 2011 14:15:09 -0700 Subject: [PATCH] add treeToString method to General --- src/General.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/General.v b/src/General.v index 100da75..e1e5791 100644 --- a/src/General.v +++ b/src/General.v @@ -129,7 +129,14 @@ Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A), reflexivity. Qed. - +Open Scope string_scope. +Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string := +match t with + | T_Leaf None => "[]" + | T_Leaf (Some s) => "["+++s+++"]" + | T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2 +end. +Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }. (*******************************************************************************) (* Lists *) -- 1.7.10.4