# HG changeset patch # User haftmann # Date 1121330899 -7200 # Node ID 0a28f033de03634bd8ea68cf3f896e4d2ebcdf91 # Parent c889f499911ca10ad4f7db73b7eb3961dec6e3a0 added ` combinator diff -r c889f499911c -r 0a28f033de03 src/Pure/library.ML --- a/src/Pure/library.ML Thu Jul 14 10:32:01 2005 +0200 +++ b/src/Pure/library.ML Thu Jul 14 10:48:19 2005 +0200 @@ -8,7 +8,7 @@ tables, balanced trees, orders, current directory, misc. *) -infix |> |-> ||> ||>> |>> |>>> #> #-> `> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto +infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto mem mem_int mem_string union union_int union_string inter inter_int inter_string subset subset_int subset_string; @@ -29,7 +29,7 @@ val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd) val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd - val `> : 'b * ('b -> 'a) -> 'a * 'b + val ` : ('b -> 'a) -> 'b -> 'a * 'b val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b @@ -310,7 +310,7 @@ fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end; fun f #> g = g o f; fun f #-> g = fn s => let val (v, s') = f s in g v s' end; -fun x `> h = (h x, x) +fun ` h = fn s => (h s, s) (*composition with multiple args*) fun (f oo g) x y = f (g x y);