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