list_mk_imp
boolSyntax.list_mk_imp : term list * term -> term
Iteratively constructs implications.
list_mk_imp([t1,...,tn],t) returns t1 ==> ( ... (tn ==> t)...).
Failure
Fails if any of t1,...,tn are not of type bool. Also fails if the
list of terms is non-empty and t is not of type bool. If the list of
terms is empty the type of t can be anything.
Example
> list_mk_imp ([T,F],T);
val it = “T ⇒ F ⇒ T”: term
> try list_mk_imp ([T,F],mk_var("x",alpha));
Exception- HOL_ERR (at boolSyntax.mk_imp: Non-boolean argument) raised
> list_mk_imp ([],mk_var("x",alpha));
val it = “x”: term