1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
\DOC list_mk_forall
\TYPE {list_mk_forall : term list * term -> term}
\SYNOPSIS
Iteratively constructs a universal quantification.
\DESCRIBE
{list_mk_forall([`x1`;...;`xn`],`t`)} returns {`!x1 ... xn. t`}.
\FAILURE
Fails if any term in the list is not a variable or if {t} is not of type
{`:bool`} and the list of terms is non-empty. If the list of terms is empty the
type of {t} can be anything.
\EXAMPLE
{
# list_mk_forall([`x:num`; `y:num`],`x + y + 1 = SUC z`);;
val it : term = `!x y. x + y + 1 = SUC z`
}
\SEEALSO
mk_forall, strip_forall.
\ENDDOC
|
