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