src/Pure/library.ML
changeset 32188 005f9abae1e3
parent 31986 a68f88d264f7
child 32352 4839a704939a
equal deleted inserted replaced
32187:cca43ca13f4f 32188:005f9abae1e3
   107   val ~~ : 'a list * 'b list -> ('a * 'b) list
   107   val ~~ : 'a list * 'b list -> ('a * 'b) list
   108   val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
   108   val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
   109   val split_list: ('a * 'b) list -> 'a list * 'b list
   109   val split_list: ('a * 'b) list -> 'a list * 'b list
   110   val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   110   val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   111   val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   111   val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   112   val multiply: 'a list -> 'a list list -> 'a list list
       
   113   val separate: 'a -> 'a list -> 'a list
   112   val separate: 'a -> 'a list -> 'a list
   114   val surround: 'a -> 'a list -> 'a list
   113   val surround: 'a -> 'a list -> 'a list
   115   val replicate: int -> 'a -> 'a list
   114   val replicate: int -> 'a -> 'a list
   116   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
   115   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
   117   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   116   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   550   in
   549   in
   551     if n < 0 then raise Subscript
   550     if n < 0 then raise Subscript
   552     else rep (n, [])
   551     else rep (n, [])
   553   end;
   552   end;
   554 
   553 
   555 (*multiply [a, b, c, ...] * [xs, ys, zs, ...]*)
       
   556 fun multiply [] _ = []
       
   557   | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
       
   558 
   554 
   559 (* direct product *)
   555 (* direct product *)
   560 
   556 
   561 fun map_product f _ [] = []
   557 fun map_product f _ [] = []
   562   | map_product f [] _ = []
   558   | map_product f [] _ = []
  1136   constructors at any time*)
  1132   constructors at any time*)
  1137 structure Object = struct type T = exn end;
  1133 structure Object = struct type T = exn end;
  1138 
  1134 
  1139 end;
  1135 end;
  1140 
  1136 
  1141 structure BasicLibrary: BASIC_LIBRARY = Library;
  1137 structure Basic_Library: BASIC_LIBRARY = Library;
  1142 open BasicLibrary;
  1138 open Basic_Library;