dest_let : term -> term * term
STRUCTURE
boolSyntax
SYNOPSIS
Breaks apart a let-expression.
DESCRIPTION
If M is a term of the form LET M N, then dest_let M returns (M,N).
EXAMPLE
- dest_let (Term `let x = P /\ Q in x \/ x`);
> val it = (`\x. x \/ x`, `P /\ Q`) : term * term

FAILURE
Fails if M is not of the form LET M N.
SEEALSO
mk_let, is_let
HOL  Kananaskis-14