mk_gabs : term * term -> term
Constructs a generalized abstraction.
Given a pair of terms s and t, the call mk_gabs(s,t) constructs a
canonical `generalized abstraction' that is thought of as `some function that
always maps s to t'. In the case where s is a variable, the result is an
ordinary abstraction as constructed by mk_abs. In other cases, the canonical
composite structure is created. Note that the logical construct is welldefined
even if there is no function mapping s to t, and this function will
always succeed, even if the resulting structure is not really useful.
- FAILURE CONDITIONS
Here is a simple abstraction:
and here are a couple of potentially useful generalized ones:
val it : term = `\x. ~x`
while here is a vacuous one about which nothing interesting will be
proved, because there is no welldefined function that always maps x + y to
# mk_gabs(`(x:num,y:num)`,`x + y + 1`);;
val it : term = `\(x,y). x + y + 1`
# mk_gabs(`CONS (h:num) t`,`if h = 0 then t else CONS h t`);;
val it : term = `\CONS h t. if h = 0 then t else CONS h t`
# mk_gabs(`x + y:num`,`x:num`);;
val it : term = `\(x + y). x`
- SEE ALSO
dest_gabs, GEN_BETA_CONV, is_gabs, list_mk_gabs.