strip_anylet : term -> (term * term) list list * term
STRUCTURE
pairSyntax
SYNOPSIS
Repeatedly destructs arbitrary let terms.
DESCRIPTION
The invocation strip_anylet M where M has the form of a let-abstraction, i.e., LET P Q, returns a pair ([[(a1,b1),...,(an,bn)], ... [(u1,v1),...,(uk,vk)]],body), where the first element of the pair is a list of lists of bindings, and the second is the body of the let. The binding lists are required since let terms can, in general, be of the form (using surface syntax) let a1 = b1 and ... and an = bn in body.
FAILURE
Never fails.
EXAMPLE
- strip_anylet ``let g x = A in
                 let v = g x y in
                 let f x y (a,b) = g a
                 and foo = M
                 in
                  f x foo v``;
> val it =
    ([[(`g x`, `A`)],
      [(`v`, `g x y`)],
      [(`f x y (a,b)`, `g a`), (`foo`, `M`)]], `f x foo v`)
USES
Programming that involves manipulation of term syntax.
SEEALSO
dest_let, mk_anylet, list_mk_anylet, dest_anylet
HOL  Trindemossen-1