put "foldl" and "foldr" in "Useful";
authorblanchet
Wed, 15 Sep 2010 15:44:24 +0200
changeset 39409 782477d78f63
parent 39408 65a379f4c8f3
child 39410 a055cffcf6fc
put "foldl" and "foldr" in "Useful"; Isabelle hides those symbols from List, but by adding them to Useful we have them throughout Metis without "List." prefix
src/Tools/Metis/src/Useful.sig
src/Tools/Metis/src/Useful.sml
--- a/src/Tools/Metis/src/Useful.sig	Wed Sep 15 15:15:49 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sig	Wed Sep 15 15:44:24 2010 +0200
@@ -107,6 +107,10 @@
 (* Lists: note we count elements from 0.                                     *)
 (* ------------------------------------------------------------------------- *)
 
+val foldl : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b (* MODIFIED by Jasmin Blanchette *)
+
+val foldr : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b (* MODIFIED by Jasmin Blanchette *)
+
 val cons : 'a -> 'a list -> 'a list
 
 val hdTl : 'a list -> 'a * 'a list
--- a/src/Tools/Metis/src/Useful.sml	Wed Sep 15 15:15:49 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sml	Wed Sep 15 15:44:24 2010 +0200
@@ -170,6 +170,10 @@
 (* Lists.                                                                    *)
 (* ------------------------------------------------------------------------- *)
 
+val foldl = List.foldl; (* MODIFIED by Jasmin Blanchette *)
+
+val foldr = List.foldr; (* MODIFIED by Jasmin Blanchette *)
+
 fun cons x y = x :: y;
 
 fun hdTl l = (hd l, tl l);