dest_anylet : term -> (term * term) list * term
STRUCTURE
pairSyntax
SYNOPSIS
Destructs arbitrary let terms.
DESCRIPTION
The invocation dest_anylet M where M has the form of a let-abstraction, i.e., LET P Q, returns a pair ([(a1,b1),...,(an,bn)],body), where the first argument is a list of bindings, and the second is the body of the let. The list of bindings is required since let terms can, in general, be of the form (using surface syntax) let a1 = b1 and ... and an = bn in body.

Each ai can be a varstruct (a single variable or a tuple of variables), or a function variable applied to a sequence of varstructs.

FAILURE
Fails if M is not a let abstraction.
EXAMPLE
- dest_anylet ``let f (x,y) = M and g z = N in g (f (a,b))``;
> val it = ([(`f (x,y)`, `M`), (`g z`, `N`)], `g (f (a,b))`) :

- dest_anylet ``let f (x,y) = M in
                let g z = N
                in g (f (a,b))``;
> val it = ([(`f (x,y)`, `M`)], `let g z = N in g (f (a,b))`)
USES
Programming that involves manipulation of term syntax.
SEEALSO
dest_let, mk_anylet, list_mk_anylet, strip_anylet
HOL  Kananaskis-14