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
26
27
|
\DOC strip_abs
\TYPE {strip_abs : term -> term list * term}
\SYNOPSIS
Iteratively breaks apart abstractions.
\DESCRIBE
{strip_abs `\x1 ... xn. t`} returns {([`x1`;...;`xn`],`t`)}. Note that
{
strip_abs(list_mk_abs([`x1`;...;`xn`],`t`))
}
\noindent will not return {([`x1`;...;`xn`],`t`)} if {t} is an abstraction.
\FAILURE
Never fails.
\EXAMPLE
{
# strip_abs `\x y z. x /\ y /\ z`;;
val it : term list * term = ([`x`; `y`; `z`], `x /\ y /\ z`)
}
\SEEALSO
list_mk_abs, dest_abs.
\ENDDOC
|
