projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
f788a28
)
add treeToString method to General
author
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 19 Mar 2011 21:15:09 +0000
(14:15 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 19 Mar 2011 21:15:09 +0000
(14:15 -0700)
src/General.v
patch
|
blob
|
history
diff --git
a/src/General.v
b/src/General.v
index
100da75
..
e1e5791
100644
(file)
--- 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.
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 *)
(*******************************************************************************)
(* Lists *)