1\DOC W 2 3\TYPE {W : ('a -> 'a -> 'b) -> 'a -> 'b} 4 5\KEYWORDS 6Combinator. 7 8\SYNOPSIS 9Duplicates function argument : {W f x} equals {f x x}. 10 11\DESCRIBE 12The {W} combinator can be understood as a planner: in the application 13{f x x}, the function {f} can scrutinize {x} and generate a function 14that then gets applied to {x}. 15 16\FAILURE 17{W f} never fails. {W f x} fails if {f x} fails or if {f x x} fails. 18 19\EXAMPLE 20{ 21- load "tautLib"; 22- tautLib.TAUT_PROVE (Term `(a = b) = (~a = ~b)`); 23> val it = |- (a = b) = (~a = ~b) : thm 24 25- W (GENL o free_vars o concl) it; 26> val it = |- !b a. (a = b) = (~a = ~b) : thm 27} 28 29 30\SEEALSO 31Lib.##, Lib.C, Lib.I, Lib.K, Lib.S. 32\ENDDOC 33