1\DOC list_mk_imp
2
3\TYPE {list_mk_imp : term list * term -> term}
4
5\SYNOPSIS
6Iteratively constructs implications.
7
8\DESCRIBE
9{list_mk_imp([t1,...,tn],t)} returns {t1 ==> ( ... (tn ==> t)...)}.
10
11\FAILURE
12Fails if any of {t1},...,{tn} are not of type {bool}. Also fails
13if the list of terms is non-empty and {t} is not of type {bool}. If the
14list of terms is empty the type of {t} can be anything.
15
16\EXAMPLE
17{
18- list_mk_imp ([T,F],T);
19> val it = `T ==> F ==> T` : term
20
21
22- try list_mk_imp ([T,F],mk_var("x",alpha));
23evaluation failed     list_mk_imp
24
25- list_mk_imp ([],mk_var("x",alpha));
26> val it = `x` : term
27}
28
29
30\SEEALSO
31boolSyntax.strip_imp, boolSyntax.mk_imp.
32\ENDDOC
33