add ToString instance for lists
authorAdam Megacz <megacz@cs.berkeley.edu>
Sat, 14 May 2011 03:28:54 +0000 (20:28 -0700)
committerAdam Megacz <megacz@cs.berkeley.edu>
Sat, 14 May 2011 03:28:54 +0000 (20:28 -0700)
src/General.v

index db77f34..f97989d 100644 (file)
@@ -469,6 +469,15 @@ Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
   apply eqd_dec.
   Defined.
 
+Fixpoint listToString {T:Type}{tst:ToString T}(l:list T) : string :=
+  match l with
+    | nil  => "nil"
+    | a::b => (toString a) +++ "::" +++ listToString b
+  end.
+
+Instance ListToString {T:Type}{tst:ToString T} : ToString (list T) :=
+  { toString := @listToString _ _ }.
+
 (*******************************************************************************)
 (* Tree Flags                                                                  *)