list_mk_gabs : term list * term -> term
- SYNOPSIS
-
Iteratively makes a generalized abstraction.
- DESCRIPTION
-
The call list_mk_gabs([vs1; ...; vsn],t) constructs an interated generalized
abstraction \vs1. \vs2. ... \vsn. t. See mk_gabs for more details on
constructing generalized abstractions.
- FAILURE CONDITIONS
-
Never fails.
- EXAMPLE
-
# list_mk_gabs([`(x:num,y:num)`; `(w:num,z:num)`],`x + w + 1`);;
val it : term = `\(x,y). \(w,z). x + w + 1`
- SEE ALSO
-
dest_gabs, is_gabs, mk_gabs.